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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe