Restrictions on associated types for classes

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
14 messages Options
Reply | Threaded
Open this post in threaded view
|

Restrictions on associated types for classes

Stephen Lavelle-2
Given

class MyClass k where
  type AssociatedType k :: *

Is there a way of requiring AssociatedType be of class Eq, say?
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrictions on associated types for classes

MigMit
{-# LANGUAGE GADTs, TypeFamilies #-}
module Assoc where
data EqD k where EqD :: Eq k => EqD k
class MyClass k where
     data AssociatedType k :: *
     evidence :: AssociatedType k -> EqD (AssociatedType k)
eq :: MyClass k => AssociatedType k -> AssociatedType k -> Bool
-- eq k1 k2 = k1 == k2 -- doesn't work
eq k1 k2 = case evidence k1 of EqD -> k1 == k2 -- works fine

On 17 Dec 2009, at 16:37, Stephen Lavelle wrote:

> class MyClass k where
>  type AssociatedType k :: *

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrictions on associated types for classes

MigMit
Along the same lines:

{-# LANGUAGE GADTs, TypeFamilies #-}
module Assoc where
data EqD k where EqD :: Eq k => EqD k
class MyClass k where
    type AssociatedType k :: *
    evidence :: k -> EqD (AssociatedType k)
instance MyClass () where
     type AssociatedType () = Integer
     evidence _ = EqD
eq :: MyClass k => k -> AssociatedType k -> AssociatedType k -> Bool
-- eq k k1 k2 = k1 == k2 -- doesn't work
eq k k1 k2 = case evidence k of EqD -> k1 == k2 -- works fine

On 17 Dec 2009, at 17:10, Miguel Mitrofanov wrote:

> {-# LANGUAGE GADTs, TypeFamilies #-}
> module Assoc where
> data EqD k where EqD :: Eq k => EqD k
> class MyClass k where
>    data AssociatedType k :: *
>    evidence :: AssociatedType k -> EqD (AssociatedType k)
> eq :: MyClass k => AssociatedType k -> AssociatedType k -> Bool
> -- eq k1 k2 = k1 == k2 -- doesn't work
> eq k1 k2 = case evidence k1 of EqD -> k1 == k2 -- works fine

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrictions on associated types for classes

Tom Schrijvers-2
In reply to this post by Stephen Lavelle-2
> class MyClass k where
>  type AssociatedType k :: *
>
> Is there a way of requiring AssociatedType be of class Eq, say?

Have you tried:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}

class Eq (AssociatedType k) => MyClass k where
   type AssociatedType k :: *

?

Cheers,

Tom

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: [hidden email]
url: http://www.cs.kuleuven.be/~toms/

Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrictions on associated types for classes

Roman Leshchinskiy
In reply to this post by Stephen Lavelle-2
On 18/12/2009, at 00:37, Stephen Lavelle wrote:

> Given
>
> class MyClass k where
>  type AssociatedType k :: *
>
> Is there a way of requiring AssociatedType be of class Eq, say?

This works with -XFlexibleContexts:

class Eq (AssociatedType k) => MyClass k where
type AssociatedType k :: *


Roman


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrictions on associated types for classes

Conor McBride-2
In reply to this post by Tom Schrijvers-2
Hi all

On 17 Dec 2009, at 14:22, Tom Schrijvers wrote:

>> class MyClass k where
>> type AssociatedType k :: *
>>
>> Is there a way of requiring AssociatedType be of class Eq, say?
>
> Have you tried:
>
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE FlexibleContexts #-}
>
> class Eq (AssociatedType k) => MyClass k where
>  type AssociatedType k :: *

I just got very excited about this. I'm supposed to be
setting a test, but this is far more interesting. I tried
this

 > {-# LANGUAGE TypeFamilies, FlexibleContexts, EmptyDataDecls,  
TypeOperators #-}

 > module DDD where

 > class (Diff (D f)) => Diff f where
 >   type D f
 >   plug :: D f x -> x -> f x

 > newtype K a x = K a deriving Show

 > data Void
 > magic :: Void -> a
 > magic x = x `seq` error "haha"

 > instance Diff (K a) where
 >   type D (K a) = K Void
 >   plug (K c) x = magic c

 > newtype I x = I x deriving Show

 > instance Diff I where
 >   type D I = K ()
 >   plug (K ()) x = I x

 > data (f :+: g) x = L (f x) | R (g x) deriving Show

 > instance (Diff f, Diff g) => Diff (f :+: g) where
 >   type D (f :+: g) = D f :+: D g
 >   plug (L f') x = L (plug f' x)
 >   plug (R g') x = R (plug g' x)

 > data (f :*: g) x = f x :& g x deriving Show

 > instance (Diff f, Diff g) => Diff (f :*: g) where
 >   type D (f :*: g) = (D f :*: g) :+: (f :*: D g)
 >   plug (L (f' :& g)) x = plug f' x :& g
 >   plug (R (f :& g')) x = f :& plug g' x

But I got this message

[1 of 1] Compiling DDD              ( DDD.lhs, interpreted )

DDD.lhs:5:2:
     Cycle in class declarations (via superclasses):
       DDD.lhs:(5,2)-(7,28): class (Diff (D f)) => Diff f where {
                                 type family D f; }
Failed, modules loaded: none.

and now I have to go back to setting my class test.

Sorry for spam

Conor

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

RE: Restrictions on associated types for classes

Simon Peyton Jones
Hmm.  If you have
   class (Diff (D f)) => Diff f where

then if I have
        f :: Diff f => ...
        f = e
then the constraints available for discharging constraints arising from e are
        Diff f
        Diff (D f)
        Diff (D (D f))
        Diff (D (D (D f)))
        ...

That's a lot of constraints.  

Simon


| -----Original Message-----
| From: [hidden email] [mailto:[hidden email]] On
| Behalf Of Conor McBride
| Sent: 17 December 2009 14:48
| To: Haskell Cafe
| Subject: Re: [Haskell-cafe] Restrictions on associated types for classes
|
| Hi all
|
| On 17 Dec 2009, at 14:22, Tom Schrijvers wrote:
|
| >> class MyClass k where
| >> type AssociatedType k :: *
| >>
| >> Is there a way of requiring AssociatedType be of class Eq, say?
| >
| > Have you tried:
| >
| > {-# LANGUAGE TypeFamilies #-}
| > {-# LANGUAGE FlexibleContexts #-}
| >
| > class Eq (AssociatedType k) => MyClass k where
| >  type AssociatedType k :: *
|
| I just got very excited about this. I'm supposed to be
| setting a test, but this is far more interesting. I tried
| this
|
|  > {-# LANGUAGE TypeFamilies, FlexibleContexts, EmptyDataDecls,
| TypeOperators #-}
|
|  > module DDD where
|
|  > class (Diff (D f)) => Diff f where
|  >   type D f
|  >   plug :: D f x -> x -> f x
|
|  > newtype K a x = K a deriving Show
|
|  > data Void
|  > magic :: Void -> a
|  > magic x = x `seq` error "haha"
|
|  > instance Diff (K a) where
|  >   type D (K a) = K Void
|  >   plug (K c) x = magic c
|
|  > newtype I x = I x deriving Show
|
|  > instance Diff I where
|  >   type D I = K ()
|  >   plug (K ()) x = I x
|
|  > data (f :+: g) x = L (f x) | R (g x) deriving Show
|
|  > instance (Diff f, Diff g) => Diff (f :+: g) where
|  >   type D (f :+: g) = D f :+: D g
|  >   plug (L f') x = L (plug f' x)
|  >   plug (R g') x = R (plug g' x)
|
|  > data (f :*: g) x = f x :& g x deriving Show
|
|  > instance (Diff f, Diff g) => Diff (f :*: g) where
|  >   type D (f :*: g) = (D f :*: g) :+: (f :*: D g)
|  >   plug (L (f' :& g)) x = plug f' x :& g
|  >   plug (R (f :& g')) x = f :& plug g' x
|
| But I got this message
|
| [1 of 1] Compiling DDD              ( DDD.lhs, interpreted )
|
| DDD.lhs:5:2:
|      Cycle in class declarations (via superclasses):
|        DDD.lhs:(5,2)-(7,28): class (Diff (D f)) => Diff f where {
|                                  type family D f; }
| Failed, modules loaded: none.
|
| and now I have to go back to setting my class test.
|
| Sorry for spam
|
| Conor
|
| _______________________________________________
| Haskell-Cafe mailing list
| [hidden email]
| http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrictions on associated types for classes

Jacques Carette
Which is 'right' in a way, since in the language Conor defined, all
definable terms are "infinitely differentiable", and that can be
inferred from the given rules.  That, in practice, you only need a
finite number of them in any given computation is derivable from the
instances, but is not a general theorem.

Jacques

PS: wait until someone wants to define resurgent functions, where you
need ordinals to keep track of similar information!  Nice thing is that
it's all still computable, you just have to work a fair bit harder to
set up the correct machinery.  See papers by Salvy & Shackell, as well
as van der Hoeven.

Simon Peyton-Jones wrote:

> Hmm.  If you have
>    class (Diff (D f)) => Diff f where
>
> then if I have
> f :: Diff f => ...
> f = e
> then the constraints available for discharging constraints arising from e are
> Diff f
> Diff (D f)
> Diff (D (D f))
> Diff (D (D (D f)))
> ...
>
> That's a lot of constraints.  
>
> Simon
>
>
> | -----Original Message-----
> | From: [hidden email] [mailto:[hidden email]] On
> | Behalf Of Conor McBride
> | Sent: 17 December 2009 14:48
> | To: Haskell Cafe
> | Subject: Re: [Haskell-cafe] Restrictions on associated types for classes
> |
> | Hi all
> |
> | On 17 Dec 2009, at 14:22, Tom Schrijvers wrote:
> |
> | >> class MyClass k where
> | >> type AssociatedType k :: *
> | >>
> | >> Is there a way of requiring AssociatedType be of class Eq, say?
> | >
> | > Have you tried:
> | >
> | > {-# LANGUAGE TypeFamilies #-}
> | > {-# LANGUAGE FlexibleContexts #-}
> | >
> | > class Eq (AssociatedType k) => MyClass k where
> | >  type AssociatedType k :: *
> |
> | I just got very excited about this. I'm supposed to be
> | setting a test, but this is far more interesting. I tried
> | this
> |
> |  > {-# LANGUAGE TypeFamilies, FlexibleContexts, EmptyDataDecls,
> | TypeOperators #-}
> |
> |  > module DDD where
> |
> |  > class (Diff (D f)) => Diff f where
> |  >   type D f
> |  >   plug :: D f x -> x -> f x
> |
> |  > newtype K a x = K a deriving Show
> |
> |  > data Void
> |  > magic :: Void -> a
> |  > magic x = x `seq` error "haha"
> |
> |  > instance Diff (K a) where
> |  >   type D (K a) = K Void
> |  >   plug (K c) x = magic c
> |
> |  > newtype I x = I x deriving Show
> |
> |  > instance Diff I where
> |  >   type D I = K ()
> |  >   plug (K ()) x = I x
> |
> |  > data (f :+: g) x = L (f x) | R (g x) deriving Show
> |
> |  > instance (Diff f, Diff g) => Diff (f :+: g) where
> |  >   type D (f :+: g) = D f :+: D g
> |  >   plug (L f') x = L (plug f' x)
> |  >   plug (R g') x = R (plug g' x)
> |
> |  > data (f :*: g) x = f x :& g x deriving Show
> |
> |  > instance (Diff f, Diff g) => Diff (f :*: g) where
> |  >   type D (f :*: g) = (D f :*: g) :+: (f :*: D g)
> |  >   plug (L (f' :& g)) x = plug f' x :& g
> |  >   plug (R (f :& g')) x = f :& plug g' x
> |
> | But I got this message
> |
> | [1 of 1] Compiling DDD              ( DDD.lhs, interpreted )
> |
> | DDD.lhs:5:2:
> |      Cycle in class declarations (via superclasses):
> |        DDD.lhs:(5,2)-(7,28): class (Diff (D f)) => Diff f where {
> |                                  type family D f; }
> | Failed, modules loaded: none.
> |
> | and now I have to go back to setting my class test.
> |
> | Sorry for spam
> |
> | Conor
> |
> | _______________________________________________
> | Haskell-Cafe mailing list
> | [hidden email]
> | http://www.haskell.org/mailman/listinfo/haskell-cafe
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>  

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrictions on associated types for classes

Conor McBride-2
In reply to this post by Simon Peyton Jones

On 17 Dec 2009, at 15:31, Simon Peyton-Jones wrote:

> Hmm.  If you have
>   class (Diff (D f)) => Diff f where
>
> then if I have
> f :: Diff f => ...
> f = e
> then the constraints available for discharging constraints arising  
> from e are
> Diff f
> Diff (D f)
> Diff (D (D f))
> Diff (D (D (D f)))
> ...
>
> That's a lot of constraints.

But isn't it a bit like having an instance

   Diff f => Diff (D f)

?

Conor
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

RE: Restrictions on associated types for classes

Simon Peyton Jones
| > Hmm.  If you have
| >   class (Diff (D f)) => Diff f where
| >
| > then if I have
| > f :: Diff f => ...
| > f = e
| > then the constraints available for discharging constraints arising
| > from e are
| > Diff f
| > Diff (D f)
| > Diff (D (D f))
| > Diff (D (D (D f)))
| > ...
| >
| > That's a lot of constraints.
|
| But isn't it a bit like having an instance
|
|    Diff f => Diff (D f)

A little bit.  And indeed, could you not provide such instances?  That is, every time you write an equation for D, such as
        type D (K a) = K Void
make sure that Diff (K Void) also holds.

The way you it, when you call f :: Diff f => <blah>, you are obliged to pass runtime evidence that (Diff f) holds.  And that runtime evidence includes as a sub-component runtime evidence that (Diff (D f)) holds.   If you like the, the evidence for Diff f looks like this:
        data Diff f = MkDiff (Diff (D f)) (D f x -> x -> f x)
So you are going to have to build an infinite data structure.  You can do that fine in Haskell, but type inference looks jolly hard.

For example, suppose we are seeking evidence for
        Diff (K ())
We might get such evidence from either
  a) using the instance decl
         instance Diff (K a) where ...
or
  b) using the fact that (D I) ~ K (), we need Diff I, so
        we could use the instance
          instance Diff I

Having two ways to get the evidence seems quite dodgy to me, even apart from the fact that I have no clue how to do type inference for it.

Simon
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrictions on associated types for classes

Stephen Lavelle-2
In reply to this post by Roman Leshchinskiy
Ah yes, this is very very very helpful.  Thanks : )

Miguel's example is not quite as idiomatic, but...for some reason I
find it beguiling nonetheless.

On Thu, Dec 17, 2009 at 2:36 PM, Roman Leshchinskiy <[hidden email]> wrote:

> On 18/12/2009, at 00:37, Stephen Lavelle wrote:
>
>> Given
>>
>> class MyClass k where
>>  type AssociatedType k :: *
>>
>> Is there a way of requiring AssociatedType be of class Eq, say?
>
> This works with -XFlexibleContexts:
>
> class Eq (AssociatedType k) => MyClass k where
> type AssociatedType k :: *
>
>
> Roman
>
>
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrictions on associated types for classes

Martin Sulzmann-3
In reply to this post by Simon Peyton Jones
The statements

class Cl [a] => Cl a

and

instance Cl a => Cl [a]

(I omit the type family constructor in the head for simplicyt)

state the same (logical) property:

For each Cl t there must exist Cl [t].

Their operational meaning is different under the dictionary-passing translation [1].
The instance declaration says we build dictionary Cl [a] given the
dictionary Cl [a]. The super class declaration says that the dictionary for Cl [a]
must be derivable (extractable) from Cl a's dictionary. So, here
we run into a cycle (on the level of terms as well as type inference).

However, if we'd adopt a type-passing translation [2] (similar to
dynamic method lookup in oo languages) then there isn't
necessarily a cycle (for terms and type inference). Of course,
we still have to verify the 'cyclic' property which smells like
we run into non-termination if we assume some inductive reason
(but we might be fine applying co-induction).

-Martin

[1] Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, Philip Wadler: Type Classes in Haskell. ACM Trans. Program. Lang. Syst. 18(2): 109-138 (1996)

[2] Satish R. Thatte: Semantics of Type Classes Revisited. LISP and Functional Programming 1994: 208-219

On Thu, Dec 17, 2009 at 6:40 PM, Simon Peyton-Jones <[hidden email]> wrote:
| > Hmm.  If you have
| >   class (Diff (D f)) => Diff f where
| >
| > then if I have
| >     f :: Diff f => ...
| >     f = e
| > then the constraints available for discharging constraints arising
| > from e are
| >     Diff f
| >     Diff (D f)
| >     Diff (D (D f))
| >     Diff (D (D (D f)))
| >     ...
| >
| > That's a lot of constraints.
|
| But isn't it a bit like having an instance
|
|    Diff f => Diff (D f)

A little bit.  And indeed, could you not provide such instances?  That is, every time you write an equation for D, such as
       type D (K a) = K Void
make sure that Diff (K Void) also holds.

The way you it, when you call f :: Diff f => <blah>, you are obliged to pass runtime evidence that (Diff f) holds.  And that runtime evidence includes as a sub-component runtime evidence that (Diff (D f)) holds.   If you like the, the evidence for Diff f looks like this:
       data Diff f = MkDiff (Diff (D f)) (D f x -> x -> f x)
So you are going to have to build an infinite data structure.  You can do that fine in Haskell, but type inference looks jolly hard.

For example, suppose we are seeking evidence for
       Diff (K ())
We might get such evidence from either
 a) using the instance decl
        instance Diff (K a) where ...
or
 b) using the fact that (D I) ~ K (), we need Diff I, so
       we could use the instance
         instance Diff I

Having two ways to get the evidence seems quite dodgy to me, even apart from the fact that I have no clue how to do type inference for it.

Simon
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrictions on associated types for classes

Dan Weston
I think the denotational meanings are different. The instance also implies:

For each Cl t there must exist a Cl u where u does not unify with [v]
for some v.
In other words, there must be a ground instance.

For the class declaration, the existence of a ground instance can be
inferred only by excluding infinite types with strict type unification
semantics. If infinite types were admitted (where type unification is
done non-strictly), the class declaration allows for infinite types (let
t ~ [t] in t). The instance does not.

Dan

Martin Sulzmann wrote:

> The statements
>
> class Cl [a] => Cl a
>
> and
>
> instance Cl a => Cl [a]
>
> (I omit the type family constructor in the head for simplicyt)
>
> state the same (logical) property:
>
> For each Cl t there must exist Cl [t].
>
> Their operational meaning is different under the dictionary-passing
> translation [1].
> The instance declaration says we build dictionary Cl [a] given the
> dictionary Cl [a]. The super class declaration says that the dictionary
> for Cl [a]
> must be derivable (extractable) from Cl a's dictionary. So, here
> we run into a cycle (on the level of terms as well as type inference).
>
> However, if we'd adopt a type-passing translation [2] (similar to
> dynamic method lookup in oo languages) then there isn't
> necessarily a cycle (for terms and type inference). Of course,
> we still have to verify the 'cyclic' property which smells like
> we run into non-termination if we assume some inductive reason
> (but we might be fine applying co-induction).
>
> -Martin
>
> [1] Cordelia V. Hall, Kevin Hammond
> <http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/h/Hammond:Kevin.html>,
> Simon L. Peyton Jones
> <http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/j/Jones:Simon_L=_Peyton.html>,
> Philip Wadler
> <http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wadler:Philip.html>:
> Type Classes in Haskell. ACM Trans. Program. Lang. Syst. 18
> <http://www.informatik.uni-trier.de/%7Eley/db/journals/toplas/toplas18.html#HallHJW96>(2):
> 109-138 (1996)
>
> [2] Satish R. Thatte: Semantics of Type Classes Revisited. LISP and
> Functional Programming 1994
> <http://www.informatik.uni-trier.de/%7Eley/db/conf/lfp/lfp1994.html#Thatte94>:
> 208-219
>
> On Thu, Dec 17, 2009 at 6:40 PM, Simon Peyton-Jones
> <[hidden email] <mailto:[hidden email]>> wrote:
>
>     | > Hmm.  If you have
>     | >   class (Diff (D f)) => Diff f where
>     | >
>     | > then if I have
>     | >     f :: Diff f => ...
>     | >     f = e
>     | > then the constraints available for discharging constraints arising
>     | > from e are
>     | >     Diff f
>     | >     Diff (D f)
>     | >     Diff (D (D f))
>     | >     Diff (D (D (D f)))
>     | >     ...
>     | >
>     | > That's a lot of constraints.
>     |
>     | But isn't it a bit like having an instance
>     |
>     |    Diff f => Diff (D f)
>
>     A little bit.  And indeed, could you not provide such instances?
>      That is, every time you write an equation for D, such as
>            type D (K a) = K Void
>     make sure that Diff (K Void) also holds.
>
>     The way you it, when you call f :: Diff f => <blah>, you are obliged
>     to pass runtime evidence that (Diff f) holds.  And that runtime
>     evidence includes as a sub-component runtime evidence that (Diff (D
>     f)) holds.   If you like the, the evidence for Diff f looks like this:
>            data Diff f = MkDiff (Diff (D f)) (D f x -> x -> f x)
>     So you are going to have to build an infinite data structure.  You
>     can do that fine in Haskell, but type inference looks jolly hard.
>
>     For example, suppose we are seeking evidence for
>            Diff (K ())
>     We might get such evidence from either
>      a) using the instance decl
>             instance Diff (K a) where ...
>     or
>      b) using the fact that (D I) ~ K (), we need Diff I, so
>            we could use the instance
>              instance Diff I
>
>     Having two ways to get the evidence seems quite dodgy to me, even
>     apart from the fact that I have no clue how to do type inference for it.
>
>     Simon
>     _______________________________________________
>     Haskell-Cafe mailing list
>     [hidden email] <mailto:[hidden email]>
>     http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restrictions on associated types for classes

Dan Weston
Oops, reverse that. The *instance* declaration allows for infinite
types, the *class* declaration does not.

Dan Weston wrote:

> I think the denotational meanings are different. The instance also implies:
>
> For each Cl t there must exist a Cl u where u does not unify with [v]
> for some v.
> In other words, there must be a ground instance.
>
> For the class declaration, the existence of a ground instance can be
> inferred only by excluding infinite types with strict type unification
> semantics. If infinite types were admitted (where type unification is
> done non-strictly), the class declaration allows for infinite types (let
> t ~ [t] in t). The instance does not.
>
> Dan
>
> Martin Sulzmann wrote:
>> The statements
>>
>> class Cl [a] => Cl a
>>
>> and
>>
>> instance Cl a => Cl [a]
>>
>> (I omit the type family constructor in the head for simplicyt)
>>
>> state the same (logical) property:
>>
>> For each Cl t there must exist Cl [t].
>>
>> Their operational meaning is different under the dictionary-passing
>> translation [1].
>> The instance declaration says we build dictionary Cl [a] given the
>> dictionary Cl [a]. The super class declaration says that the dictionary
>> for Cl [a]
>> must be derivable (extractable) from Cl a's dictionary. So, here
>> we run into a cycle (on the level of terms as well as type inference).
>>
>> However, if we'd adopt a type-passing translation [2] (similar to
>> dynamic method lookup in oo languages) then there isn't
>> necessarily a cycle (for terms and type inference). Of course,
>> we still have to verify the 'cyclic' property which smells like
>> we run into non-termination if we assume some inductive reason
>> (but we might be fine applying co-induction).
>>
>> -Martin
>>
>> [1] Cordelia V. Hall, Kevin Hammond
>> <http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/h/Hammond:Kevin.html>,
>> Simon L. Peyton Jones
>> <http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/j/Jones:Simon_L=_Peyton.html>,
>> Philip Wadler
>> <http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wadler:Philip.html>:
>> Type Classes in Haskell. ACM Trans. Program. Lang. Syst. 18
>> <http://www.informatik.uni-trier.de/%7Eley/db/journals/toplas/toplas18.html#HallHJW96>(2):
>> 109-138 (1996)
>>
>> [2] Satish R. Thatte: Semantics of Type Classes Revisited. LISP and
>> Functional Programming 1994
>> <http://www.informatik.uni-trier.de/%7Eley/db/conf/lfp/lfp1994.html#Thatte94>:
>> 208-219
>>
>> On Thu, Dec 17, 2009 at 6:40 PM, Simon Peyton-Jones
>> <[hidden email] <mailto:[hidden email]>> wrote:
>>
>>     | > Hmm.  If you have
>>     | >   class (Diff (D f)) => Diff f where
>>     | >
>>     | > then if I have
>>     | >     f :: Diff f => ...
>>     | >     f = e
>>     | > then the constraints available for discharging constraints arising
>>     | > from e are
>>     | >     Diff f
>>     | >     Diff (D f)
>>     | >     Diff (D (D f))
>>     | >     Diff (D (D (D f)))
>>     | >     ...
>>     | >
>>     | > That's a lot of constraints.
>>     |
>>     | But isn't it a bit like having an instance
>>     |
>>     |    Diff f => Diff (D f)
>>
>>     A little bit.  And indeed, could you not provide such instances?
>>      That is, every time you write an equation for D, such as
>>            type D (K a) = K Void
>>     make sure that Diff (K Void) also holds.
>>
>>     The way you it, when you call f :: Diff f => <blah>, you are obliged
>>     to pass runtime evidence that (Diff f) holds.  And that runtime
>>     evidence includes as a sub-component runtime evidence that (Diff (D
>>     f)) holds.   If you like the, the evidence for Diff f looks like this:
>>            data Diff f = MkDiff (Diff (D f)) (D f x -> x -> f x)
>>     So you are going to have to build an infinite data structure.  You
>>     can do that fine in Haskell, but type inference looks jolly hard.
>>
>>     For example, suppose we are seeking evidence for
>>            Diff (K ())
>>     We might get such evidence from either
>>      a) using the instance decl
>>             instance Diff (K a) where ...
>>     or
>>      b) using the fact that (D I) ~ K (), we need Diff I, so
>>            we could use the instance
>>              instance Diff I
>>
>>     Having two ways to get the evidence seems quite dodgy to me, even
>>     apart from the fact that I have no clue how to do type inference for it.
>>
>>     Simon
>>     _______________________________________________
>>     Haskell-Cafe mailing list
>>     [hidden email] <mailto:[hidden email]>
>>     http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe