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 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 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

John Van Enk wrote:

...

Haskell not having 'polymorphic kinds'.

Is there a good description of why Haskell doesn't have polymorphic kinds?

IANA expert but polymorphic kinds belong to a set of reasonably new influences (e.g. from dependently typed programming languages and generic programming) and they haven't been 1) polished enough to be a widely accepted standard or 2) simply haven't been implemented yet (low priority, etc). Besides that, I sometimes see polymorphic kinds in GHC error messages, so I suspect that at least parts of GHC already support them. Martijn.

Thats a bit farther down the rabbit hole than the concern in question, though certainly related. An example of what you could write with polymorphic kinds, inventing a notation for polymorphic kind variables using 'x to denote a polymorphic kind x, which could subtitute in for a kind k = * | ** | k -> k | ... type Id (f :: 'k) = f type Const (a :: 'a) (b :: 'b) = a data True data False type family If c (x :: 'k) (y :: 'k) :: 'k type instance If True x y = x type instance If False x y = y then you could safely apply Id and If types of different kinds. class Container x where type Elem x :: * type SearchOffersMultipleResults x :: * search :: x -> SearchResult x type SearchResult x = (If (SearchOffersMultipleResults x) [] Maybe) (Elem x) instance Container (SomeContainer a) where type Elem (SomeContainer a) = a type SearchOffersMultipleResults (SomeContainer a) = True I suppose once down this slippery slope you might consider classes that are parameterized on types with polymorphic kinds as well, but I definitely wouldn't start there. ;) -Edward On Mon, Mar 30, 2009 at 2:54 PM, John Van Enk wrote:

I suppose having a good description of what I'd like to do might help: I'd like to be able to make an N-Tuple an instance of a type class.

class Foo a where ....

instance Foo (,) where ....

instance Foo (,,) where .... The different kindedness of (,) and (,,) prevent this from working.

/jve

On Mon, Mar 30, 2009 at 2:00 PM, Martijn van Steenbergen < martijn@van.steenbergen.nl> wrote:

...

John Van Enk wrote:

...

...

Haskell not having 'polymorphic kinds'. Is there a good description of why Haskell doesn't have polymorphic kinds?

IANA expert but polymorphic kinds belong to a set of reasonably new influences (e.g. from dependently typed programming languages and generic programming) and they haven't been 1) polished enough to be a widely accepted standard or 2) simply haven't been implemented yet (low priority, etc).

Besides that, I sometimes see polymorphic kinds in GHC error messages, so I suspect that at least parts of GHC already support them.

Martijn.

-- /jve

I wasn't questioning the utility of John's library. But I saw him mentioning unary numbers and I think it's a mistake to use those for anything practical involving even moderately sized numbers. I'd love to see a good type level programming library. There's a lot of it out there, but it's never packaged in a way that is reusable as a good library. -- Lennart 2009/3/30 Edward Kmett :

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 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 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

On Mon, 2009-03-30 at 20:54 +0100, Lennart Augustsson wrote:

I wasn't questioning the utility of John's library. But I saw him mentioning unary numbers and I think it's a mistake to use those for anything practical involving even moderately sized numbers.

Also agreed! tfp supports rational arithmetic through its decimal numbers, and in my opinion, a new library should build upon tfp, adding features like the regular prelude H.O.F.s until there is a prelude for types. - John Morrice