[Haskell-cafe] partially applied data constructor and corresponding type
TP
paratribulations at free.fr
Mon Apr 29 08:55:29 CEST 2013
Thanks for pointing to "type level integers". With that I have found:
http://www.haskell.org/haskellwiki/The_Monad.Reader/Issue5/Number_Param_Types
For example:
-------------------------------
data Zero = Zero
data Succ a = Succ a
class Card c where
c2num:: c -> Integer
cpred::(Succ c) -> c
cpred = undefined
instance Card Zero where
c2num _ = 0
instance (Card c) => Card (Succ c) where
c2num x = 1 + c2num (cpred x)
main = do
putStrLn $ show $ c2num (Succ (Succ Zero))
-------------------------------
I will continue to examine the topic in the following days, according to my
needs.
Thanks a lot,
TP
On Sunday, April 28, 2013 07:58:58 Stephen Tetley wrote:
> What you probably want are type level integers (naturals)
>
> Yury Sulsky used them in the message above - basically you can't use
> literal numbers 1,2,3,... etc as they are values of type Int (or
> Integer, etc...) instead you have to use type level numbers:
>
> data One
> data Two
>
> Work is ongoing for type level numbers in GHC and there are user
> libraries on Hackage so there is a lot of work to crib from.
More information about the Haskell-Cafe
mailing list