Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement Monad instances for Either, Maybe and List #37

Closed
jstolarek opened this Issue Apr 23, 2014 · 9 comments

Comments

Projects
None yet
2 participants
@jstolarek
Copy link
Collaborator

commented Apr 23, 2014

  • export them from Prelude
@jstolarek

This comment has been minimized.

Copy link
Collaborator Author

commented Apr 25, 2014

Richard, I'm stuck on this one. I defined open type classes to represent monadic functions:

type family (:>>=) (a :: k1) (b :: TyFun k2 k1 -> *) :: k1
type family (:>>)  (a :: k1) (b :: k1) :: k1
type family Return (a :: k1) :: k2
$(genDefunSymbols [ ''(:>>=), ''(:>>), ''Return ])

Then I define instances. For example Maybe:

$(promoteOnly [d|
    maybeReturn            :: a -> Maybe a
    maybeReturn a          = Just a

    maybeBind              :: Maybe a -> (a -> Maybe a) -> Maybe a
    maybeBind (Just x) k   = k x
    maybeBind Nothing  _   = Nothing

    maybeBind'             :: Maybe a -> Maybe a -> Maybe a
    maybeBind' (Just _) k  = k
    maybeBind' Nothing  _  = Nothing
 |])

type instance Return a = MaybeReturn a
type instance a :>>= b = MaybeBind   a b
type instance a :>>  b = MaybeBind'  a b

Now here's a test:

$(promote [d|
  data Foo = A | B | C | D

  fooM1 :: Maybe Foo
  fooM1 = return A

  fooM2 :: Maybe Foo
  fooM2 = fooM1 >>= return
 |])

fooM1a :: Proxy FooM1
fooM1a = Proxy

fooM1b :: Proxy (Just A)
fooM1b = fooM1a

fooM2a :: Proxy FooM2
fooM2a = Proxy

fooM2b :: Proxy (Just A)
fooM2b = fooM2a

FooM1 works but FooM2 fails with:

Couldn't match type `'Just 'A :>>= ReturnSym0` with `'Just 'A`
Expected type: Proxy ('Just 'A)
  Actual type: Proxy FooM2
In the expression: fooM2a
In an equation for `fooM2b`: fooM2b = fooM2a

It looks that application of :>>= does not reduce but I can't figure out why. I tried more liberal definitions of :>>= like type family (:>>=) (a :: k1) (b :: k2) :: k3 with no effect. Help?

@goldfirere

This comment has been minimized.

Copy link
Owner

commented Apr 25, 2014

I was afraid something like this might happen.

First off, it looks like some of the declared types are slightly wrong. Here is I would write these definitions:

type family (:>>=) (a :: k1) (b :: TyFun k k2 -> *) :: k2
type family (:>>)  (a :: k1) (b :: k2) :: k2
type family Return (a :: k1) :: k2
$(genDefunSymbols [ ''(:>>=), ''(:>>), ''Return ])

$(promoteOnly [d|
  maybeReturn            :: a -> Maybe a
  maybeReturn a          = Just a

  maybeBind              :: Maybe a -> (a -> Maybe b) -> Maybe b
  maybeBind (Just x) k   = k x
  maybeBind Nothing  _   = Nothing

  maybeBind'             :: Maybe a -> Maybe b -> Maybe b    
  maybeBind' (Just _) k  = k
  maybeBind' Nothing  _  = Nothing
|])

But, that’s not what’s broken. What’s broken (and can’t obviously be fixed) is the type of (:>>=), even as I’ve given it. That type makes no connection between k1 (which should be m a) and k (which should be a). In the foo2 example, GHC can figure out that k1 should be Maybe Foo and k2 should be Maybe Foo, but it’s mystified on how to instantiate k. Without the right instantiation for k, GHC can’t use the type instance you’ve provided, and the type family is stuck. This becomes more apparent with -fprint-explicit-kinds.

The solution, in this case, is to say this:

  fooM2 = fooM1 >>= (return :: Foo -> Maybe Foo)

Now, GHC knows what to do and can proceed.

How to solve in the general case? I haven’t the foggiest idea. If ScopedTypeVariables actually worked sanely (see comments in Single.Monad.bindTyVars for this explanation), I think this would be fixable. As it stands, I’m not sure what the best solution is. Let me ponder a while and get back to you.

On Apr 25, 2014, at 4:23 AM, Jan Stolarek notifications@github.com wrote:

Richard, I'm stuck on this one. I defined open type classes to represent monadic functions:

type family (:>>=) (a :: k1) (b :: TyFun k2 k1 -> *) :: k1
type family (:>>) (a :: k1) (b :: k1) :: k1
type family Return (a :: k1) :: k2
$(genDefunSymbols [ ''(:>>=), ''(:>>), ''Return ])
Then I define instances. For example Maybe:

$(promoteOnly [d|
maybeReturn :: a -> Maybe a
maybeReturn a = Just a

maybeBind              :: Maybe a -> (a -> Maybe a) -> Maybe a
maybeBind (Just x) k   = k x
maybeBind Nothing  _   = Nothing

maybeBind'             :: Maybe a -> Maybe a -> Maybe a
maybeBind' (Just _) k  = k
maybeBind' Nothing  _  = Nothing

|])

type instance Return a = MaybeReturn a
type instance a :>>= b = MaybeBind a b
type instance a :>> b = MaybeBind' a b
Now here's a test:

$(promote [d|
data Foo = A | B | C | D

fooM1 :: Maybe Foo
fooM1 = return A

fooM2 :: Maybe Foo
fooM2 = fooM1 >>= return
|])

fooM1a :: Proxy FooM1
fooM1a = Proxy

fooM1b :: Proxy (Just A)
fooM1b = fooM1a

fooM2a :: Proxy FooM2
fooM2a = Proxy

fooM2b :: Proxy (Just A)
fooM2b = fooM2a
FooM1 works but FooM2 fails with:

Couldn't match type 'Just 'A :>>= ReturnSym0 with 'Just 'A
Expected type: Proxy ('Just 'A)
Actual type: Proxy FooM2
In the expression: fooM2a
In an equation for fooM2b: fooM2b = fooM2a
It looks that application of :>>= does not reduce but I can't figure out why. I tried more liberal definitions of :>>= like type family (:>>=) (a :: k1) (b :: k2) :: k3 with no effect. Help?


Reply to this email directly or view it on GitHub.

@goldfirere

This comment has been minimized.

Copy link
Owner

commented Apr 27, 2014

Well, I've pondered, and I'm stuck.

There seem to be two ways of fixing a problem like this, and I'm convinced neither of them work.

Way 1: Fix the type family / type instances so that GHC can do the right thing at use sites. First off, this fix must be in the type family, not instances, because GHC hasn't selected an instance by the time it must do something differently than its current behavior. And, GHC doesn't have kind families nor higher-sorted kind variables, so there's not much we can do in the family definition. If only a type family could have functional dependencies, we could get somewhere, but alas, no. (Sidenote: of course, a type family can be declared within a class with functional dependencies, but GHC doesn't apply the fundeps when examining the type family.)

Way 2: Beef up our promotion algorithm to give GHC enough hints to get this right. The problem is that this amounts to type inference, which is a Terrible Idea. The way we would have to do this is to poke around looking for, say, some function that returns a Maybe, realize that we're in the Maybe monad, and then mechanically replace (:>>=) with MaybeBind everywhere. Some silly, ad-hoc approach might work, but it would be fragile. We could perhaps require users to use an explicit type annotation with every do, and then inspect the annotation and propagate the information. (Note, these ideas are just simple subsets of type inference.)

What next? We decide that (a) this is too important to be left out and then decide on some fragile heuristics in order to specialize the monadic combinators during promotion or (b) describe this as a limitation of our approach and an incentive to get GHC to fix its higher-sorted kind variables / functional dependencies in type families / lack of kind families.

(Of course, I'm working on implementing higher-sorted kind variables and kind families, among other goodies, but that's a separate story.)

What do you think?

@jstolarek

This comment has been minimized.

Copy link
Collaborator Author

commented Apr 27, 2014

it looks like some of the declared types are slightly wrong

Ah, yes. I noticed that later but it also didn't work.

(b) describe this as a limitation of our approach and an incentive to get GHC to fix its higher-sorted kind variables / functional dependencies in type families / lack of kind families.

+1 on this one. So we need to say that we don't really support do-notation and list comprehensions, although if user annotates every monadic computation with types then all should work, right?

see comments in Single.Monad.bindTyVars for this explanation

Haha: "kinds of ty_foo and ty_bar match that of the outer context". Wasn't this supposed to be "surrounding scope" :-) Anyway, for me this comment is a bit out of context (no pun intended) but at least I know the source of all this let-defined lambda in singletonized functions.

goldfirere pushed a commit that referenced this issue Apr 27, 2014

@goldfirere goldfirere added the wontfix label Apr 27, 2014

@goldfirere

This comment has been minimized.

Copy link
Owner

commented Apr 27, 2014

OK. I'm tempted to leave this ticket "open" because it remains an issue. If you think it adds bad clutter, feel free to override this decision.

@jstolarek

This comment has been minimized.

Copy link
Collaborator Author

commented Apr 27, 2014

Is there any chance this will be fixable in foreseeable future? If no I'd document that in readme (do we actually have user documentation other than haddock?) and close the ticket.

My failed attempts are on promote-monad branch.

@goldfirere

This comment has been minimized.

Copy link
Owner

commented Apr 27, 2014

OK. I will do this shortly.

goldfirere pushed a commit that referenced this issue Apr 27, 2014

Richard Eisenberg
Update to README, fixing #37 as wontfix.
README still needs more updating. This commit just focused on
the list of supported features.

goldfirere pushed a commit that referenced this issue Apr 27, 2014

Richard Eisenberg

@goldfirere goldfirere closed this Apr 27, 2014

@goldfirere

This comment has been minimized.

Copy link
Owner

commented Oct 15, 2016

Going to reopen this, as it's now possible. I have no plans to implement the solution, but it's only for lack of time, not lack of desire.

@goldfirere

This comment has been minimized.

Copy link
Owner

commented May 31, 2017

This is now subsumed by #184. The discussion here is obsolete, so I'm closing this ticket in favor of that one.

@goldfirere goldfirere closed this May 31, 2017

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.