[Haskell-cafe] writing a function to make a correspondance between type-level integers and value-level integers
TP
paratribulations at free.fr
Sun Jun 9 12:39:12 CEST 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
More information about the Haskell-Cafe
mailing list