dependent type query

Ashley Yakeley ashley@semantic.org
Fri, 18 Jan 2002 16:11:20 -0800


At 2002-01-18 12:01, Hal Daume III wrote:

>class MyClass f a | a -> f, f -> a where ...
>
>I want to write a data type:
>
>data (MyClass f a) => MyData f = MyData (f, a)
>
>But this doesn't seem to be valid because "a" isn't in scope.

Class constraints in 'data' declarations only affect the type of 
constructor functions.

In other words, 

  data (Context) => MyData a b c = MkMyData whatever

is equivalent to

  data MyData a b c = MkMyData whatever

except for the type of MkMyData, which will be

  MkMyData :: (Context) => whatever -> MyData a b c

instead of

  MkMyData :: whatever -> MyData a b c

>  But a is uniquely determined by f.  What gives?

What you want is

  data MyData f = forall a. (MyClass f a) => MyData (f, a)

>Furthermore, I can't even write:
>
>data (MyClass f a) => MyData2 f = MyData2 f

Well now this is odd. I had no trouble simulating it with this:

  data MyData2 f = MyData2 f

  mkMyData2 :: (MyClass f a) => f -> MyData2 f
  mkMyData2 = MyData2

Looks like extended Haskell is being excessively restricted. Comments?

-- 
Ashley Yakeley, Seattle WA