Hello, I suppose Lennart is referring to type-level [1]. But type-level uses functional dependencies, right?
There is also tfp [2], which uses type families. In general, how would you say your work compares to these two? Thanks, Pedro [1] http://hackage.haskell.org/cgi-bin/hackage-scripts/package/type-level [2] http://hackage.haskell.org/cgi-bin/hackage-scripts/package/tfp On Mon, Mar 30, 2009 at 08:22, Lennart Augustsson <lenn...@augustsson.net>wrote: > There is already a library for type level number, called typelevel. > It's nice because it uses decimal representation of numbers and can > handle numbers of reasonable size. > I use it in the LLVM bindings. > > -- Lennart > > On Mon, Mar 30, 2009 at 1:07 AM, spoon <sp...@killersmurf.com> wrote: > > I've been doing some basic work on a support library for type level > > programming ( see > > http://hackage.haskell.org/trac/summer-of-code/ticket/1541 ). I know > > there have been similar attempts using fundeps ( Edward Kmett showed me > > some of his work, but I've lost the address... ) but this approach uses > > type families. > > > > Anyway, I would like to hear your critique! > > > > Currently I have higher order type functions and ad-hoc parametrized > > functions. > > > > Here's what foldl looks like: > > > > type family Foldl ( func :: * -> * -> * ) val list > > type instance Foldl func val ( Cons first rest ) = Foldl func ( Eval > > ( func val first ) ) rest > > type instance Foldl func val Nill = val > > > > Notice the use of Eval - this is a trick to enable us to pass around > > data with kind * -> *, or whatever, and then trip this into becoming a > > value. Here's an example, using this trick to define factorial: > > > > -- multiplication > > type family Times x y > > type instance Times x Zero = Zero > > type instance Times x ( Succ y ) = Sum x ( Times x y ) > > > > -- The "first order" function version of Times > > data TimesL x y > > > > -- Where what Eval forced TimesL to become. > > type instance Eval ( TimesL x y ) = Times x y > > > > -- multiplies all the elements of list of Nat together > > type Product l = > > Foldl TimesL ( Succ Zero ) l > > > > -- here list to creates a list from ( Succ Zero ) to the given number > > type Factorial x = > > Product ( ListTo x ) > > > > We can now use the function like this: > > > > *TPrelude> result ( ) :: Factorial ( Succ ( Succ ( Succ ( Zero ) ) ) ) > > Succ (Succ (Succ (Succ (Succ (Succ Zero))))) > > > > Using the parametrized types kinda reminds me of programming in Erlang: > > > > -- What would conventionally be the monad type class, parametized over m > > type family Bind m ma ( f :: * -> * ) > > type family Return m a > > type family Sequence m ma mb > > > > Here's the maybe monad: > > > > -- Monad instance > > type instance Bind ( Maybe t ) Nothing f = Nothing > > type instance Bind ( Maybe t ) ( Just a ) f = Eval ( f a ) > > type instance Sequence ( Maybe t ) Nothing a = Nothing > > type instance Sequence ( Maybe t ) ( Just a ) b = b > > type instance Return ( Maybe t ) a = Just a > > > > type instance Eval ( Just x ) = Just x > > > > Here's an example: > > *TPrelude> result ( ) :: Bind ( Maybe Nat ) ( Just Zero ) Just > > Just Zero > > > > For more information and to download the loose collection of module > > implementing this please see: > > http://www.killersmurf.com/projects/typelib > > > > John Morrice > > > > _______________________________________________ > > Haskell-Cafe mailing list > > Haskell-Cafe@haskell.org > > http://www.haskell.org/mailman/listinfo/haskell-cafe > > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe