[Haskell-cafe] Why can't we make an instance declaration on a type synonym?

[Conor McBride]

On 3 Jan 2010, at 05:18, Daniel Fischer <daniel.is.fischer at web.de>  
wrote:

> Am Sonntag 03 Januar 2010 05:37:31 schrieb Jason Dusek:
> > Well, you can, with:
> >
> > -XTypeSynonymInstances
> >
> > though I'm not sure it addresses your specific need.
> Doesn't help him here, he would need
> instance Monad (State s) where ...
> but that would be a partially applied type synonym. He would also  
> need type level lambdas,
> type State s = /\ a -> (s -> (a,s))
> But type level lambdas and partially applied type synonyms make type  
> inference undecidable if I remember correctly (if it wasn't that,  
> they'd have other dire consequences).

Type inference is undecidable already. It's still extremely useful,  
cut with just enough type annotation and checking to resolve  
ambiguities. That creates a bunch of trade-offs to negotiate and a  
design space to explore.

Lots of dependent type systems have type-level lambda (that is, they  
have lambda), undecidable type inference, decidable type checking, and  
substantial (but inadequately rationalised) facilities for suppressing  
and recovering boring details. Nobody's campaigning to kick type-level  
lambda out of Agda.

Adding type-level lambda to Haskell would amount to admitting the  
awful truth: application is not injective. When you write a do-program  
of type t, you need to solve a constraint m x = t for m and x, to  
figure out which monad to plumb in. Pretending application is  
injective makes this easy, at the cost of requiring lots of wrapper- 
types. Type-level lambda makes this constraint highly ambiguous: Maybe  
Int is also (\ x -> x) (Maybe Int), the type of a computation in the  
identity monad. To cope, we'd need a new way to be signal such  
decompositions. Worth thinking about, perhaps, but certainly a Big Deal.

Type-level lambda is not inherently disastrous. It's just a poor fit  
with Haskell's current design.

Cheers

Conor



> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe