[Haskell-cafe] type-level integers using type families

[Bertram Felgenhauer]

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