## Abstracting on, suggested solutions

I guess I should be more constructive than just whining about how Haskell doesn't always do what I want. I do have some suggestions on how to fix things.### Explicit type applications

Let's look at a simple example again:f :: forall a . a -> a f = \ x -> x b :: Bool b = f TrueThe way I like to think of this (and what happens in ghc) is that this is shorthand for something more explicit, namely the F

_{w}version of the same thing. In F

_{w}all type abstraction and type application are explicit. Let's look at the explicit version (which is no longer Haskell).

f :: forall (a::*) . a -> a f = /\ (a::*) -> \ (x::a) -> x b :: Bool b = f @Bool TrueI'm using

`/\`for type abstraction and

`expr @type`for type application. Furthermore each binder is annotated with its type. This is what ghc translates the code to internally, this process involves figuring out what all the type abstractions and applications should be.

Not something a little more complicated (from my previous post)

class C a b where x :: a y :: b f :: (C a b) => a -> [a] f z = [x, x, z]The type of

`x`is

x :: forall a b . (C a b) => aSo whenever

`x`occurs two type applications have to be inserted (there's also a dictionary to insert, but I'll ignore that). The decorated term for

`f`(ignoring the context)

f :: forall a b . (C a b) => a -> [a] f = /\ (a::*) (b::*) -> \ (z::a) -> [ x @a @b1, x @a @b2, z]The reason for the ambiguity in type checking is that the type check cannot figure out that the

`b`is in any way connected to

`b1`and

`b2`. Because it isn't. And there's currently no way we can connect them.

So I suggest that it should be possible to use explicit type application in Haskell when you want to. The code would look like this

f :: forall a b . (C a b) => a -> [a] f z = [ x @a @b, x @a @b, z]The order of the variables in the

`forall`determines the order in which the type abstractions come, and thus determines where to put the type applications.

### Something like `abstype`

Back to my original problem with abstraction. What about if this was allowed:
class Ops t where data XString t :: * (+++) :: XString t -> XString t -> XString t instance Ops Basic where type XString Basic = String (+++) = (++)So the class declaration says I'm going to use data types (which was my final try and which works very nicely). But in the instance I provide a type synonym instead. This would be like using a

`newtype`in the instance, but without having to use the newtype constructor everywhere. The fact that it's not a real data type is only visible inside the instance declaration. The compiler could in fact make a

`newtype`and insert all the coercions. This is, of course, just a variation of the

`abstype`suggestion by Wehr and Chakravarty.

Labels: Haskell, Modules, overloading

## 2 Comments:

This comment has been removed by the author.

get Liskell to have a good module system, and use that instead? :-)

Post a Comment

<< Home