> Haskell not having 'polymorphic kinds'. Is there a good description of why Haskell doesn't have polymorphic kinds?
2009/3/30 Edward Kmett <[email protected]> > Lennart, > > I think the major emphasis that John's library has is on doing things other > than numbers well in the type system, using the type family syntax to avoid > the proliferation of intermediary names that the fundep approach yields. > > I think his type family approach for type-level monads for instance is > pretty neat and quite readable. > > The biggest problem that I see with the approach is the general lack of > availability of currying due to Haskell not having 'polymorphic kinds'. So > he'd have to use Curry combinators that are specific to both the number of > arguments at the kinds of the arguments that a function has. > > John, > > http://hackage.haskell.org/cgi-bin/hackage-scripts/package/type-int > > contains my old type level 2s and 16s complement integer code and some > machinery for manipulating type level lists a la HList. > > -Edward Kmett > > > > On Mon, Mar 30, 2009 at 3:22 AM, Lennart Augustsson < > [email protected]> 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 <[email protected]> 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 >> > [email protected] >> > http://www.haskell.org/mailman/listinfo/haskell-cafe >> > >> _______________________________________________ >> Haskell-Cafe mailing list >> [email protected] >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> > > > _______________________________________________ > Haskell-Cafe mailing list > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe > > -- /jve
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
