[Haskell-cafe] writing a function to make a correspondance between type-level integers and value-level integers

9 Jun 2013

      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)’
    In the definition of data constructor ‛P’
    In the data declaration for ‛Proxy’

----------------------
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}

-- type level integers
data Nat = Zero | Succ Nat
    deriving ( Show, Eq, Ord )

-- Singleton allowing a correspondance between type-level and value-level
-- integers.
data SNat :: Nat -> * where
    SZero :: SNat Zero
    SSucc :: SNat n -> SNat (Succ n)
deriving instance Show (SNat n)

data Proxy :: Nat -> * where
    P     :: (n::Nat) -> Proxy n

class MkSNat (n::Nat) where
    mkSNat :: Proxy n -> SNat n

instance MkSNat Zero where
    mkSNat _ = SZero

instance MkSNat (Succ n) where
    mkSNat (P (Succ n)) = SSucc (mkSNat (P n))

main = do

let one = undefined :: Proxy ('Succ 'Zero)
print one
print $ mkSNat (P one)
----------------------

Thanks,

TP

References:
-----------
[1]: https://groups.google.com/forum/?fromgroups#!topic/haskell-cafe/mGDhPqHZAz8
[2]: https://groups.google.com/d/msg/haskell-cafe/Rh65kdPkX70/T2zZpV6ZpjoJ