[Haskell-cafe] type-level integers using type families
pgavin at gmail.com
Sat May 31 11:32:52 EDT 2008
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>>>
> 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.
> 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.
More information about the Haskell-Cafe