[Haskell-cafe] Why can't we make an instance declaration on a
conor at strictlypositive.org
Sun Jan 3 04:37:05 EST 2010
On 3 Jan 2010, at 05:18, Daniel Fischer <daniel.is.fischer at web.de>
> 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.
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe