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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe