[Haskell-cafe] type-level integers using type families
Bertram Felgenhauer
bertram.felgenhauer at googlemail.com
Sun Jun 1 00:29:02 EDT 2008
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
More information about the Haskell-Cafe
mailing list