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

[jberryman]

This may be a dumb question, but why can we not declare a Monad
instance of a type synonym? This question came to me while working
with the State monad recently and feeling that the requirement that we
wrap our functions in the State constructor is a bit... kludgy.

Why can't the State monad be defined this way?:

> type State s a = \s -> (a , s)
>
> instance Monad (State s) where
> return a = \s -> (a, s)
> m >>= k = \s -> let
> (a, s') = m s
> in k a s'

It seems like Haskell's type system could understand the above, but
I'm interested in hearing the technical reason which I'm sure exists
for why we can't do this.

Thanks for any clues,
Brandon Simmons
http://coder.bsimmons.name/blog/
_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Jason Dusek]

Well, you can, with:

-XTypeSynonymInstances

though I'm not sure it addresses your specific need.

--
Jason Dusek

[Daniel Fischer]

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).

[Ivan Lazar Miljenovic]

jberryman <brandon....@gmail.com> writes:

> This may be a dumb question, but why can we not declare a Monad
> instance of a type synonym? This question came to me while working
> with the State monad recently and feeling that the requirement that we
> wrap our functions in the State constructor is a bit... kludgy.
>

Because type defines an _alias_. If you define "type Foo = Maybe Int",
then everywhere you have a "Foo" the compiler should be able to replace
it with "Maybe Int".

As such, if you have a custom instance on your type synonym (say a
custom Show instance for Foo), then which instance will the compiler
use?

--
Ivan Lazar Miljenovic
Ivan.Mi...@gmail.com
IvanMiljenovic.wordpress.com

[Conor McBride]

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

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

[Reid Barton]

On Mon, Jan 04, 2010 at 11:50:57AM -0500, Brandon Simmons wrote:

> On Sun, Jan 3, 2010 at 2:22 AM, Ivan Lazar Miljenovic
> <ivan.mi...@gmail.com> wrote:
> > jberryman <brandon....@gmail.com> writes:
> >
> >> This may be a dumb question, but why can we not declare a Monad
> >> instance of a type synonym? This question came to me while working
> >> with the State monad recently and feeling that the requirement that we
> >> wrap our functions in the State constructor is a bit... kludgy.
> >>
> >
> > Because type defines an _alias_. �If you define "type Foo = Maybe Int",
> > then everywhere you have a "Foo" the compiler should be able to replace
> > it with "Maybe Int".
> >
> > As such, if you have a custom instance on your type synonym (say a
> > custom Show instance for Foo), then which instance will the compiler
> > use?
>
>

> Thanks. I guess what I'm really asking is if there is any way to
> redefine the monad instance for (->) such that we can have a State
> monad without the data constructor wrapper.

It would be a nightmare for type inference. Consider:

return "foo" :: String -> (String, String) -- \x -> ("foo", x)

which would be valid in a language where we can do what you suggest.
`return` has type `a -> m a`, so `a` must be `String`, and now we need
to unify `String -> m String` with `String -> String -> (String, String)`.
In Haskell, these just don't unify because there are no type-level lambdas.
Even if there were, how is the typechecker supposed to know that we want
the solution `m a = String -> (a, String)` and not `m a = a -> (a, a)`
or many other possibilites?

The purpose of the newtype State is to have something to unify `m` with:

return "foo" :: State String String

We can unify `String -> m String` with `String -> State String String`
by setting `m` to `State String`.

Regards,
Reid Barton

[Brandon Simmons]

Thanks, that makes a lot of sense.

Brandon