[Haskell-cafe] Re: type versus data declarations

[Brandon S. Allbery KF8NH]

On Jun 8, 2007, at 16:25 , Emilio Jesús Gallego Arias wrote:

> Yeah, in general Haskell types don't carry constraints, however, I  
> don't
> see the reason that this doesn't work when using type level macros, as
>
>> type F a = C a => a
>
> should just be a macro and substitute.

It is.  That's the problem.

Macros can't know anything about the contexts in which they're used.   
In the type system, this translates to implicit "forall" constraints:

 > type F' a = forall a. C a => a

The result of this is that a simple use like

 > foo :: F a -> F a

expands the macros literally, with the implicit "forall" because the  
macro expansion has to assume it is independent of everything else:

 > foo' :: (forall a. C a => a) -> (forall a. C a => a)

This means the two "a"s are independent and can't be unified by the  
typechecker.

In theory I suppose the simple macro expansion could be replaced by  
some type expression which would allow the typechecker to recognize  
that any (F a)s used in a given type can be unified, but I have no  
idea what it would look like.  (Then again, I'm no type hacker.)  And  
I find myself wondering if that would lead to problems when expanding  
complex types.

-- 
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery at kf8nh.com
system administrator [openafs,heimdal,too many hats] allbery at ece.cmu.edu
electrical and computer engineering, carnegie mellon university    KF8NH