Opened 18 months ago

Closed 18 months ago

Last modified 16 months ago

#15008 closed feature request (worksforme)

Type synonyms with hidden, determined type variables

Reported by: nomeata Owned by:
Priority: normal Milestone: Research needed
Component: Compiler Version: 8.5
Keywords: QuantifiedConstraints Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

I found myself wanting to write (simplified)

type MyMonad m = (MonadReader r m, Show r)

but GHC does not accept this, it wants r as part of the type synonym. So why did I think this could work? Because MonadReader has a functional dependency:

class Monad m => MonadReader r m | m -> r

so if m determines r, why do I have to write MyMonad r m and not just MyMonad m? Can I not “hide” the fact that, somewhere internal to the MyMonad synonym, there is an additional variable r around?

Clearly supporting this would need a language proposal, but I wanted to open a ticket here first to hear if this would even be possible to implement.

(Others have wanted this before as well.)

Change History (9)

comment:1 Changed 18 months ago by Iceland_jack

I consider this solved by QuantifiedConstraints

a :: (MonadReader r m, Show r) => m String
a = fmap show ask

becomes

-- A type synonym works but is less useful
class    (forall xx. (MonadReader xx m, Show xx)) => MyMonad m
instance (forall xx. (MonadReader xx m, Show xx)) => MyMonad m

b :: MyMonad m => m String
b = fmap show ask
Last edited 18 months ago by Iceland_jack (previous) (diff)

comment:2 Changed 18 months ago by nomeata

Ah, nice!

This answers the question “is it feasible and implementable?”.

It still leaves the question “do we want to provide the convenience of a type synonym to our users” so that they don't have to encode it manually using such a class and an instance.

comment:3 Changed 18 months ago by Iceland_jack

Did you have something like that in mind?

-- user writes
type MyMonad m = (MonadReader r m, Show r)

but GHC knows that r is determined by m so silently

-- GHC transforms it into
type MyMonad m = (forall xx. (MonadReader xx m, Show xx))

comment:4 Changed 18 months ago by Iceland_jack

Keywords: QuantifiedConstraints wipT2893 added

comment:5 Changed 18 months ago by nomeata

Oh, but now you are using type, not a class/instance pair. Does the type work just fine?

If that works (with quantified constraints), then I’d be happy, as user, to write

type MyMonad m = (forall r. (MonadReader r m, Show r))

comment:6 in reply to:  5 Changed 18 months ago by Iceland_jack

That works fine unless your example requires partial application (type instance F = MyMonad)

comment:7 Changed 18 months ago by nomeata

Resolution: worksforme
Status: newclosed

That works fine

That’s good enough for me :-)

comment:8 in reply to:  3 Changed 18 months ago by AntC

Replying to Iceland_jack:

-- GHC transforms it into
type MyMonad m = (forall xx. (MonadReader xx m, Show xx))

The power of QuantifiedConstraints seems to get closer to 'magic', the more I see of them! If we didn't have a FunDep on MonadReader, could we simulate it with an implication constraint thusly?

-- user writes or GHC transforms it into
type MyMonad m = (forall xx. (MonadReader xx m, MonadReader xx m => Show xx))

Would we then need a superclass constraint Show xx on MonadReader xx m? Or would it be sufficient if the instances were for types in Show?

comment:9 Changed 16 months ago by RyanGlScott

Keywords: wipT2893 removed
Note: See TracTickets for help on using tickets.