search

coreyoconnor / type-level-tf

Type level numerics for Haskell using type families. Based on type-level.
Other
3 stars 3 forks source link

unable to resolve types in Div constructs #1

Open mikesteele81 opened 11 years ago

mikesteele81 commented 11 years ago

I'm unable to turn Div constructs into integrals:

> toNum (d2 `Data.TypeLevel.div` d1)

<interactive>:16:1:
    No instance for (Data.TypeLevel.Num.Sets.NatI
                       (Data.TypeLevel.Num.Ops.Div' D2 D1 GT))
      arising from a use of `toNum'
    Possible fix:
      add an instance declaration for
      (Data.TypeLevel.Num.Sets.NatI
         (Data.TypeLevel.Num.Ops.Div' D2 D1 GT))
    In the expression: toNum (d2 `Data.TypeLevel.div` d1)
    In an equation for `it': it = toNum (d2 `Data.TypeLevel.div` d1)
>

It looks like the problem is in Data.TypeLevel.Num.Ops:

type family Div' x y x_gt_y
type instance Div' x y False = D0
type instance Div' x y True = Succ (Div' (Sub x y) y ((Sub x y) :>=: y))  
type family Div x y
type instance Div x y = Div' x y (Trich x y)

I think I could get some output with type instance Div x y = Div' x y (x :>=: y) (I have not tried this), but that would create invalid instances. Should I expect this type-level function to mirror the behavior of Prelude's div?

Are my expectations wrong? I'm still trying to wrap my head around type-level arithmetic.

coreyoconnor commented 11 years ago

I have not tried the div instances actually. I will have to investigate. On Oct 4, 2012 2:18 PM, "Michael Steele" notifications@github.com wrote:

I'm unable to turn Div constructs into integrals:

toNum (d2 Data.TypeLevel.div d1)

:16:1: No instance for (Data.TypeLevel.Num.Sets.NatI (Data.TypeLevel.Num.Ops.Div' D2 D1 GT)) arising from a use of `toNum' Possible fix: add an instance declaration for (Data.TypeLevel.Num.Sets.NatI (Data.TypeLevel.Num.Ops.Div' D2 D1 GT)) In the expression: toNum (d2`Data.TypeLevel.div`d1) In an equation for`it': it = toNum (d2 `Data.TypeLevel.div` d1) It looks like the problem is in Data.TypeLevel.Num.Ops: type family Div' x y x_gt_y type instance Div' x y False = D0 type instance Div' x y True = Succ (Div' (Sub x y) y ((Sub x y) :>=: y)) type family Div x y type instance Div x y = Div' x y (Trich x y) I think I could get some output with type instance Div x y = Div' x y (x :>=: y) (I have not tried this), but that would create invalid instances. Should I expect this type-level function to mirror the behavior of Prelude's div? Are my expectations wrong? I'm still trying to wrap my head around type-level arithmetic. — Reply to this email directly or view it on GitHubhttps://github.com/coreyoconnor/type-level-tf/issues/1.