Sure. Here's an example.
{-# LANGUAGE TypeFamilies #-}
module Mail where
class C1 a where
data T1 a :: *
f1 :: T1 a -> T1 a
instance C1 Bool where
data T1 Bool = A | B deriving Show
f1 A = B
f1 B = A
class C2 a where
type T2 a :: *
f2 :: T2 a -> T2 a
data D2 = C | D deriving Show
instance C2 Bool where
type T2 Bool = D2
f2 C = D
f2 D = C
If you try to evaluate (f1 A) it works fine, whereas (f2 C) gives a
type error. In fact, the f2 function is impossible to use.
-- Lennart
On Wed, Dec 10, 2008 at 1:40 PM, Jules Bean
Lennart Augustsson wrote:
For an associated data type D, we know that the type function D is injective, i.e., for different indicies given to D we'll get different data types. This makes much more powerful reasoning possible in the type checker. If associated data types are removed there has to be some new mechanism to declare an associated type as injective, or the type system will lose power.
Interesting.
Are you able to give an example which exploits this "known distinct types" effect?