[Haskell-cafe] Associated data types

[Lennart Augustsson]

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?
>