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