type-level integers using type families

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
10 messages Options
Reply | Threaded
Open this post in threaded view
|

type-level integers using type families

Peter Gavin
Has anyone else tried implementing type-level integers using type families?

I tried using a couple of other type level arithmetic libraries
(including type-level on Hackage) and they felt a bit clumsy to use.  I
started looking at type families and realized I could pretty much build
an entire Scheme-like language based on them.

In short, I've got addition, subtraction, & multiplication working after
just a days worth of hacking. I'm going to post the darcs archive
sometime, sooner if anyone's interested.

I really like the type-families based approach to this, it's a lot
easier to understand, and you can think about things functionally
instead of relationally.  (Switching back and forth between Prolog-ish
thinking and Haskell gets old quick.) Plus you can do type arithmetic
directly in place, instead of using type classes everywhere.

One thing that I'd like to be able to do is lazy unification on type
instances, so that things like

data True
data False

type family Cond x y z
type instance Cond True y z = y
type instance Cond False y z = z

will work if the non-taken branch can't be unified with anything.  Is
this planned? Is it even feasible?

I'm pretty sure it would be possible to implement a Lambda like this,
but I'm not seeing it yet. Any ideas?

Pete
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: type-level integers using type families

Isaac Dupree
Peter Gavin wrote:

> Has anyone else tried implementing type-level integers using type families?
>
> I tried using a couple of other type level arithmetic libraries
> (including type-level on Hackage) and they felt a bit clumsy to use.  I
> started looking at type families and realized I could pretty much build
> an entire Scheme-like language based on them.
>
> In short, I've got addition, subtraction, & multiplication working after
> just a days worth of hacking. I'm going to post the darcs archive
> sometime, sooner if anyone's interested.
>
> I really like the type-families based approach to this, it's a lot
> easier to understand, and you can think about things functionally
> instead of relationally.  (Switching back and forth between Prolog-ish
> thinking and Haskell gets old quick.) Plus you can do type arithmetic
> directly in place, instead of using type classes everywhere.

nice, it's been tried before, etc. etc.. And of course it doesn't work
with a released version of GHC, so maybe it's hoping too much that it
would be on Hackage.  What I was going to say was, see if there is one
on hackage, otherwise there should be one there to be polished.  But I
guess searching haskell-cafe is your man :-) (your way to try to find
any.  Or the Haskell blogosphere too.)

> One thing that I'd like to be able to do is lazy unification on type
> instances, so that things like
>
> ...
>
> will work if the non-taken branch can't be unified with anything.  Is
> this planned? Is it even feasible?
>
> I'm pretty sure it would be possible to implement a Lambda like this,
> but I'm not seeing it yet. Any ideas?

Yeah -- that would be neat but generally tends to lead to undecidability
(unless you're really careful making it a lot(?) less useful).  That is,
potential nontermination in the type inferencer/checker, not just in
runtime.  Then you'll want it to be well-defined when something is
type-level-lazy, so you can reliably write your type-level algorithms.
And *that* is bound to be rather difficult to define and to implement
and maintain.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: type-level integers using type families

Manuel M T Chakravarty
In reply to this post by Peter Gavin
Peter Gavin:

> Has anyone else tried implementing type-level integers using type  
> families?
>
> I tried using a couple of other type level arithmetic libraries  
> (including type-level on Hackage) and they felt a bit clumsy to  
> use.  I started looking at type families and realized I could pretty  
> much build an entire Scheme-like language based on them.
>
> In short, I've got addition, subtraction, & multiplication working  
> after just a days worth of hacking. I'm going to post the darcs  
> archive sometime, sooner if anyone's interested.
>
> I really like the type-families based approach to this, it's a lot  
> easier to understand, and you can think about things functionally  
> instead of relationally.  (Switching back and forth between Prolog-
> ish thinking and Haskell gets old quick.) Plus you can do type  
> arithmetic directly in place, instead of using type classes  
> everywhere.

I am glad to hear that type families work for you.

> One thing that I'd like to be able to do is lazy unification on type  
> instances, so that things like
>
> data True
> data False
>
> type family Cond x y z
> type instance Cond True y z = y
> type instance Cond False y z = z
>
> will work if the non-taken branch can't be unified with anything.  
> Is this planned? Is it even feasible?

I don't think i entirely understand the question.  Do you mean that  
from an equality like

   Cond b Int Bool ~ Int

you want the type checker to infer that (b ~ True)?  This is generally  
not correct reasoning as type families are open; ie, subsequent  
modules might add

   data Bogus
   type instance Bogus y z = Int

and now there are two solutions to (Cond b Int Bool ~ Int).

Manuel

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: type-level integers using type families

Benedikt Huber
In reply to this post by Peter Gavin
Peter Gavin schrieb:

> Has anyone else tried implementing type-level integers using type families?
>
> I tried using a couple of other type level arithmetic libraries
> (including type-level on Hackage) and they felt a bit clumsy to use.  I
> started looking at type families and realized I could pretty much build
> an entire Scheme-like language based on them.
>
> In short, I've got addition, subtraction, & multiplication working after
> just a days worth of hacking. I'm going to post the darcs archive
> sometime, sooner if anyone's interested.
>
> I really like the type-families based approach to this, it's a lot
> easier to understand, and you can think about things functionally
> instead of relationally.  (Switching back and forth between Prolog-ish
> thinking and Haskell gets old quick.) Plus you can do type arithmetic
> directly in place, instead of using type classes everywhere.

I tried to rewrite Alfonso Acosta's type-level library (the one on
hackage) using type-families too, because, right, they are much nicer to
use than MPTCs.

It is a straigtforward translation, I've uploaded it to

http://code.haskell.org/~bhuber/type-level-tf-0.2.1.tar.gz

now (relevant files: src/Data/TypeLevel/{Bool.hs,Num/Ops.hs}).

I've also added a type-level ackermann to torture ghc a little bit ;),
but left out logarithms. Plus, I did very little testing.

> One thing that I'd like to be able to do is lazy unification on type instances, so that things like
>
> data True
> data False
>
> type family Cond x y z
> type instance Cond True y z = y
> type instance Cond False y z = z

I'm not sure if this is what you had in mind, but I also found that e.g.

 > type instance Mod x y = Cond (y :>: x) x  (Mod (Sub x y) y)

won't terminate, as

 > Mod D0 D1 ==> Cond True D0 (Mod (Sub D0 D1) D0) ==> <loop>

rather than

 > Mod D0 D1 ==> Cond True D0 ? ==> D0

For Mod, I used the following (usual) encoding:

 > type family Mod' x y x_gt_y
 > type instance Mod' x y False = x
 > type instance Mod' x y True  = Mod' (Sub x y) y ((Sub x y) :>=: y)
 > type family Mod x y
 > type instance Mod x y = Mod' x y (x :>=: y)

There are few other things you cannot do with type families, and some
for which you need type classes anyway (Alfonso pointed me to
http://www.haskell.org/pipermail/haskell-cafe/2008-February/039489.html 
). Here's what I found:


1) One cannot define type equality (unless total type families become
available), i.e. use the overlapping instances trick:
> instance Eq e e  True
> instance Eq e e' False

Consequently, all type-level functions which depend on type equality
(see HList) need to be encoded using type classes.

2) One cannot use superclass contexts to derive instances e.g. to define
> instance Succ (s,s') =>  Pred (s',s)

In constrast, when using MPTC + FD, one can establish more than one TL
function in one definition

 > class Succ x x' | x -> x', x' -> x

3) Not sure if this is a problem in general, but I think you cannot
restrict the set of type family instances easily.

E.g., if you have an instance

 > type instance Mod10 (x :* D0) = D0

then you also have

 > Mod10 (FooBar :* D0) ~ D0

What would be nice is something like

 > type instance (IsPos x) => Mod10 (x :* D0) = D0

though

 > type family AssertThen b x
 > type instance AssertThen True x = x
 > type instance Mod10 (x :* D0) = AssertThen (IsPos x) D0

seems to work as well.

4) Not really a limitation, but if you want to use instance methods of
Nat or Bool (e.g. toBool) on the callee site, you have to provide
context that the type level functions are closed w.r.t. to the type class:

> test_1a :: forall a b b1 b2 b3.
>           (b1 ~ And a b,
>            b2 ~ Not (Or a b),
>            b3 ~ Or b1 b2,
>            Bool b3) => a -> b -> Prelude.Bool
> test_1a a b = toBool (undefined :: b3)

Actually, I think the 'a ~ b' syntax is very nice.

I'm really looking forward to type families.

best regards,

benedikt
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: type-level integers using type families

Roberto Zunino-2
In reply to this post by Manuel M T Chakravarty
Manuel M T Chakravarty wrote:
> Peter Gavin:
>> will work if the non-taken branch can't be unified with anything.  Is
>> this planned? Is it even feasible?
>
> I don't think i entirely understand the question.

Maybe he wants, given

  cond :: Cond x y z => x -> y -> z
  tt :: True
  true_exp  :: a
  false_exp :: <<<untypable>>>

that

  cond tt true_exp false_exp :: a

That is the type of false_exp is "lazily inferred", so that type errors
do not make inference fail if they show up in an unneeded place.

If we had subtyping, typing that as Top would suffice, I believe.

Zun.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: type-level integers using type families

Peter Gavin
Roberto Zunino wrote:

> Manuel M T Chakravarty wrote:
>> Peter Gavin:
>>> will work if the non-taken branch can't be unified with anything.  Is
>>> this planned? Is it even feasible?
>> I don't think i entirely understand the question.
>
> Maybe he wants, given
>
>   cond :: Cond x y z => x -> y -> z
>   tt :: True
>   true_exp  :: a
>   false_exp :: <<<untypable>>>
>
> that
>
>   cond tt true_exp false_exp :: a
>
> That is the type of false_exp is "lazily inferred", so that type errors
> do not make inference fail if they show up in an unneeded place.

Yes, that's exactly what I want, but for type families (not MPTC). I
think it could be done if the type arguments were matched one at a time,
across all visible instances.

So given

 > data True
 > data False
 >
 > type family Cond x y z
 > type instance Cond True y z = y
 > type instance Cond False y z = z

the first argument (x) of Cond would be matched before y and z are
inferred. Then if x is True, the type checker would see that z is never
used on the RHS, so it would not bother trying to infer it at all.

>
> If we had subtyping, typing that as Top would suffice, I believe.
>
> Zun.
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: type-level integers using type families

Peter Gavin
In reply to this post by Benedikt Huber
Benedikt Huber wrote:

>> data True
>> data False
>>
>> type family Cond x y z
>> type instance Cond True y z = y
>> type instance Cond False y z = z
>
> I'm not sure if this is what you had in mind, but I also found that e.g.
>
>  > type instance Mod x y = Cond (y :>: x) x  (Mod (Sub x y) y)
>
> won't terminate, as
>
>  > Mod D0 D1 ==> Cond True D0 (Mod (Sub D0 D1) D0) ==> <loop>

Right, because it always tries to infer the (Mod (Sub x y) y) part no
matter what the result of (y :>: x) is.

>
> rather than
>
>  > Mod D0 D1 ==> Cond True D0 ? ==> D0
>
> For Mod, I used the following (usual) encoding:
>
>  > type family Mod' x y x_gt_y
>  > type instance Mod' x y False = x
>  > type instance Mod' x y True  = Mod' (Sub x y) y ((Sub x y) :>=: y)
>  > type family Mod x y
>  > type instance Mod x y = Mod' x y (x :>=: y)
>

Yes, it's possible to terminate a loop by matching the type argument
directly.

> 1) One cannot define type equality (unless total type families become
> available), i.e. use the overlapping instances trick:
>> instance Eq e e  True
>> instance Eq e e' False

I didn't want to mix type classes and families in my implementation. All
the predicates are implemented like so:

 > type family Eq x y
 > type instance Eq D0 D0 = True
 > type instance Eq D1 D1 = True
...
 > type instance Eq (xh :* xl) (yh :* yl) = And (Eq xl yl) (Eq xh yh)

then I've added a single type-class

 > class Require b
 > instance Require True

so you can do stuff like

 > f :: (Require (Eq (x :+: y) z)) => x -> y -> z

or whatever.  I haven't yet tested it (but I think it should work) :)

Pete

>
> Consequently, all type-level functions which depend on type equality
> (see HList) need to be encoded using type classes.
>
> 2) One cannot use superclass contexts to derive instances e.g. to define
>> instance Succ (s,s') =>  Pred (s',s)
>
> In constrast, when using MPTC + FD, one can establish more than one TL
> function in one definition
>
>  > class Succ x x' | x -> x', x' -> x
>
> 3) Not sure if this is a problem in general, but I think you cannot
> restrict the set of type family instances easily.
>
> E.g., if you have an instance
>
>  > type instance Mod10 (x :* D0) = D0
>
> then you also have
>
>  > Mod10 (FooBar :* D0) ~ D0
>
> What would be nice is something like
>
>  > type instance (IsPos x) => Mod10 (x :* D0) = D0
>
> though
>
>  > type family AssertThen b x
>  > type instance AssertThen True x = x
>  > type instance Mod10 (x :* D0) = AssertThen (IsPos x) D0
>
> seems to work as well.
>
> 4) Not really a limitation, but if you want to use instance methods of
> Nat or Bool (e.g. toBool) on the callee site, you have to provide
> context that the type level functions are closed w.r.t. to the type class:
>
>> test_1a :: forall a b b1 b2 b3.
>>           (b1 ~ And a b,
>>            b2 ~ Not (Or a b),
>>            b3 ~ Or b1 b2,
>>            Bool b3) => a -> b -> Prelude.Bool
>> test_1a a b = toBool (undefined :: b3)
>
> Actually, I think the 'a ~ b' syntax is very nice.
>
> I'm really looking forward to type families.
>
> best regards,
>
> benedikt

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: type-level integers using type families

Peter Gavin
In reply to this post by Peter Gavin
Replying to myself...

I put a copy of the darcs repo at <http://code.haskell.org/~pgavin/tfp>,
if anyone is interested.

Pete

Peter Gavin wrote:

> Has anyone else tried implementing type-level integers using type families?
>
> I tried using a couple of other type level arithmetic libraries
> (including type-level on Hackage) and they felt a bit clumsy to use.  I
> started looking at type families and realized I could pretty much build
> an entire Scheme-like language based on them.
>
> In short, I've got addition, subtraction, & multiplication working after
> just a days worth of hacking. I'm going to post the darcs archive
> sometime, sooner if anyone's interested.
>
> I really like the type-families based approach to this, it's a lot
> easier to understand, and you can think about things functionally
> instead of relationally.  (Switching back and forth between Prolog-ish
> thinking and Haskell gets old quick.) Plus you can do type arithmetic
> directly in place, instead of using type classes everywhere.
>
> One thing that I'd like to be able to do is lazy unification on type
> instances, so that things like
>
> data True
> data False
>
> type family Cond x y z
> type instance Cond True y z = y
> type instance Cond False y z = z
>
> will work if the non-taken branch can't be unified with anything.  Is
> this planned? Is it even feasible?
>
> I'm pretty sure it would be possible to implement a Lambda like this,
> but I'm not seeing it yet. Any ideas?
>
> Pete

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: type-level integers using type families

Bertram Felgenhauer-2
In reply to this post by Peter Gavin
Peter Gavin wrote:

> Roberto Zunino wrote:
>> Maybe he wants, given
>>   cond :: Cond x y z => x -> y -> z
>>   tt :: True
>>   true_exp  :: a
>>   false_exp :: <<<untypable>>>
>> that
>>   cond tt true_exp false_exp :: a
>> That is the type of false_exp is "lazily inferred", so that type errors
>> do not make inference fail if they show up in an unneeded place.
>
> Yes, that's exactly what I want, but for type families (not MPTC). I think
> it could be done if the type arguments were matched one at a time, across
> all visible instances.

What do you think of the following idea?

Using naive type level natural numbers,

> data Zero
> newtype Succ a = Succ a

Booleans,

> data True
> data False

comparison,

> type family (:<:) x y
> type instance (Zero   :<: Succ a) = True
> type instance (Zero   :<: Zero  ) = False
> type instance (Succ a :<: Zero  ) = False
> type instance (Succ a :<: Succ b) = a :<: b

difference,

> type family Minus x y
> type instance Minus a        Zero     = a
> type instance Minus (Succ a) (Succ b) = Minus a b

and a higher order type level conditional,

> type family Cond2 x :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> *
> type First2  (x :: * -> * -> *) (y :: * -> * -> *) = x
> type Second2 (x :: * -> * -> *) (y :: * -> * -> *) = y
> type instance Cond2 True  = First2
> type instance Cond2 False = Second2

we can define division as follows:

> type family Div x y
> type DivZero x y = Zero
> type DivStep x y = Succ (Div (Minus0 x y) y)
> type instance Div x y = Cond2 (x :<: y) DivZero DivStep x y

It's not exactly what you asked for, but I believe it gets the effect
that you wanted.

Enjoy,

Bertram
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: type-level integers using type families

Bugzilla from alfonso.acosta@gmail.com
In reply to this post by Peter Gavin
On Thu, May 29, 2008 at 5:15 AM, Peter Gavin <[hidden email]> wrote:
> Has anyone else tried implementing type-level integers using type families?

When I started to work on thetype-level and parameterized data
packages,  I considered using type-families and GADTs, but I found
quite a few problems which have been nicely summarized by Benedikt in
this thread.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe