9 Jun 12:39 2013

## writing a function to make a correspondance between type-level integers and value-level integers

TP <paratribulations <at> free.fr>

2013-06-09 10:39:12 GMT

2013-06-09 10:39:12 GMT

Hi all, Following a discussion on Haskell-Cafe, Richard E. made the following proposition of a "Singleton" to make a correspondance between type-level integers and value-level integers: """ > data SNat :: Nat -> * where > SZero :: SNat 'Zero > SSucc :: SNat n -> SNat ('Succ n) """ (found at [1], and an example of application can be found at [2], also proposed by Richard E.) Now I asked myself if there is some means to write a function that would take any value of type e.g. `Succ (Succ Zero)`, and would return the value `SSucc (SSucc SZero)`. I have tried hard, but did not succeed (see below). I am constantly refrained by the fact a function or data constructor cannot take a value of type having a kind different from `*` (if I am right). Is there any solution to this problem? Below is my attempt, which yields a compilation error test_typeinteger_valueinteger_conversion.hs:18:14: Expected a type, but ‛n’ has kind ‛Nat’ In the type ‛(n :: Nat)’(Continue reading)