Associated data types

Eyal Lotem

10 Dec 2008 10 Dec '08

8:12 a.m.

If we have associated type synonyms, is there still reason to have associated data types? For example, we can replace: class C b where data D b ... instance C Int where data D Int = D | E with: class C b where type D b ... data DInt = D | E instance C Int where type D Int = DInt Or perhaps allow, for convenience, this form (which would desugar to the above): class C b where type D b ... instance C Int where data D Int = D | E

Attachments:

attachment.html (text/html — 640 bytes)

Show replies by date

Lennart Augustsson

10 Dec 10 Dec

8:36 a.m.

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. -- Lennart 2008/12/10 Eyal Lotem :

...

If we have associated type synonyms, is there still reason to have associated data types?

For example, we can replace:

class C b where data D b ...

instance C Int where data D Int = D | E

with:

class C b where type D b ...

data DInt = D | E instance C Int where type D Int = DInt

Or perhaps allow, for convenience, this form (which would desugar to the above):

class C b where type D b ...

instance C Int where data D Int = D | E _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Jules Bean

8:40 a.m.

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?

Lennart Augustsson

9:09 a.m.

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

Andres Loeh

9:17 a.m.

Hi.

...

Date: Wed, 10 Dec 2008 13:36:11 +0000 From: Lennart Augustsson Subject: Re: [Haskell-cafe] Associated data types

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.

-- Lennart

2008/12/10 Eyal Lotem :

...
If we have associated type synonyms, is there still reason to have associated data types?

[...] Another, somewhat related, issue is that associated type synonyms cannot currently be partially applied, whereas associated data types can. Cheers, Andres -- Andres Loeh, Universiteit Utrecht mailto:andres@cs.uu.nl mailto:mail@andres-loeh.de http://www.andres-loeh.de

6007

Age (days ago)

6007

Last active (days ago)

List overview

Download

4 comments

4 participants

participants (4)

Andres Loeh
Eyal Lotem
Jules Bean
Lennart Augustsson