[Haskell-cafe] Associated data types
Lennart Augustsson
lennart at augustsson.net
Wed Dec 10 09:09:23 EST 2008
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 <jules at jellybean.co.uk> wrote:
> 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?
>
More information about the Haskell-Cafe
mailing list