Fwd: EvTerms and how they are used

[Jan Bracker]

Hi Adam,

again thank you for your extensive and patient answer!

It's a bit hard to know exactly what is going on without the full code,
> but I think what is happening is this: you have an unsolved constraint
> `Polymonad Identity n_abpq Identity` and your plugin provides an
> evidence term of type `Polymonad Identity Identity Identity`, but of
> course this is ill-typed, because `n_abpq` is not `Identity`. Hence Core
> Lint quite reasonably complains.
>

I would have thought the constraint solver would derive that 'obviously'
`n_abpq` needs to be unified with `Identity` and substitutes.


> I'm not sure exactly what you are trying to do, but I think the right
> way to approach this problem is to simulate a functional dependency on
> Polymonad (in fact, can you use an actual functional dependency)?


That is exactly what I _don't_ want to do. I am trying to achieve a more
general version of monads, called polymonads as it was introduced here [1].


> When confronted with the constraint `Polymonad Identity n_abpq Identity`,
> do
> not try to solve it directly, but instead notice that you must have
> `n_abpq ~ Identity`. Your plugin can emit this as an additional derived
> constraint, which will allow GHC's built-in solver to instantiate the
> unification variable `n_abpq` and then solve the original constraint
> using the existing instance. No manual evidence generation needed!
>

Yes, that makes perfect sense! I was so gridlocked, I did not see this as a
possibility to solve the problem.

Out of interest, can you say anything about your aims here? I'm keen to
> find out about the range of applications of typechecker plugins.
>

I want to make Polymonads as proposed in [1] usable in Haskell. They
generalize
the bind operator to a more general signature `M a -> (a -> N b) -> P b`.
Polymonads
subsume the standard Monad as well as indexed or parameterized monad,
without
relying on functional dependencies, which can be limiting (there may be
different
requirement depending on the monad being implemented).
Currently I am providing a type class for this:

class Polymonad m n p where
  (>>=) :: m a -> (a -> n b) -> p b

As the paper points out in section 4.2 (Ambiguity), type inference breaks
down,
because the constraint solver is not able to solve the ambiguity. Here a
small example:

-- Return operator for the IO polymonad
instance Polymonad Identity Identity IO where
  -- ...

-- Identity polymonad
instance Polymonad Identity Identity Identity where
  -- ...

return :: (Polymonad Identity Identity m) => a -> m a
return x = Identity x >>= Identity

test :: Identity Bool
test = do
  x <- return True
  return x

For this example GHC already gives the following ambiguity errors:

Main.hs:134:3:
    No instance for (Polymonad m0 n0 Identity)
      arising from a do statement
    The type variables ‘m0’, ‘n0’ are ambiguous
    Note: there is a potential instance available:
      instance Polymonad Identity Identity Identity
        -- Defined in ‘Polymonad’
    In a stmt of a 'do' block: x <- return True
    In the expression:
      do { x <- return True;
           return x }
    In an equation for ‘test’:
        test
          = do { x <- return True;
                 return x }

Main.hs:134:8:
    No instance for (Polymonad Identity Identity m0)
      arising from a use of ‘return’
    The type variable ‘m0’ is ambiguous
    Note: there are several potential instances:
      instance Polymonad Identity Identity Identity
        -- Defined in ‘Polymonad’
      instance Polymonad Identity Identity IO -- Defined at Main.hs:85:10
    In a stmt of a 'do' block: x <- return True
    In the expression:
      do { x <- return True;
           return x }
    In an equation for ‘test’:
        test
          = do { x <- return True;
                 return x }

Main.hs:135:3:
    No instance for (Polymonad Identity Identity n0)
      arising from a use of ‘return’
    The type variable ‘n0’ is ambiguous
    Note: there are several potential instances:
      instance Polymonad Identity Identity Identity
        -- Defined in ‘Polymonad’
      instance Polymonad Identity Identity IO -- Defined at Main.hs:85:10
    In a stmt of a 'do' block: return x
    In the expression:
      do { x <- return True;
           return x }
    In an equation for ‘test’:
        test
          = do { x <- return True;
                 return x }

Of course, in the given example we can fix the ambiguity by adding type
annotations.
But as soon as the examples become bigger that is not possible anymore.

Using the approach of the paper [1] these constraints are solvable
unambiguously.
That's what I am working on.

All the best,
Jan

[1]: http://arxiv.org/pdf/1406.2060v1.pdf

On 26/02/15 10:07, Jan Bracker wrote:
> > Hi Adam,
> >
> > thank you for your quick and detailed answer! I think I understand how
> > to construct evidence for typeclass constraints now. But trying to apply
> > this, I still have some problems.
> >
> > I have something along the following lines:
> >
> > class Polymonad m n p where
> >   -- Functions
> >
> > instance Polymonad Identity Identity Identity where
> >   -- Implementation
> >
> > -- Further instances and some small chunk of code involving them:
> >
> > The code implies the following constraint:
> > Polymonad Identity n_abpq Identity
> >
> > As the ambiguity error I get says, when trying to compile this: There is
> > only one matching instance (the one above, lets call
> > it $fPolymonadIdentityIdentityIdentity).
> >
> > So my plugin tries to tell GHC to use that instance. As far as I
> > understand it, since the parameters
> > of $fPolymonadIdentityIdentityIdentity are no type variables and there
> > is no superclass it should be as easy as saying:
> > EvDFunApp $fPolymonadIdentityIdentityIdentity [] []
> >
> > But when I run this with -dcore-lint I get the following error message:
> >
> > *** Core Lint errors : in result of Desugar (after optimization) ***
> > <no location info>: Warning:
> >     In the expression: >>
> >                          @ Identity
> >                          @ Any
> >                          @ Identity
> >                          $fPolymonadIdentityIdentityIdentity
> >                          @ ()
> >                          @ ()
> >                          (idOp @ Bool True)
> >                          (>>=
> >                             @ Identity
> >                             @ Identity
> >                             @ Any
> >                             $fPolymonadIdentityIdentityIdentity
> >                             @ Char
> >                             @ ()
> >                             (return
> >                                @ Char @ Identity
> > $fPolymonadIdentityIdentityIdentity (C# 'a'))
> >                             (\ _ [Occ=Dead] ->
> >                                return @ () @ Identity
> > $fPolymonadIdentityIdentityIdentity ()))
> >     Argument value doesn't match argument type:
> >     Fun type:
> >         Polymonad Identity Any Identity =>
> >         forall a_abdV[sk] b_abdW[sk].
> >         Identity a_abdV[sk] -> Any b_abdW[sk] -> Identity b_abdW[sk]
> >     Arg type: Polymonad Identity Identity Identity
> >     Arg: $fPolymonadIdentityIdentityIdentity
> >
> > What am I missing? Why doesn't the argument type "Polymonad Identity
> > Identity Identity" match the first argument of the function type
> > "Polymonad Identity Any Identity => forall a_abdV[sk] b_abdW[sk].
> > Identity a_abdV[sk] -> Any b_abdW[sk] -> Identity b_abdW[sk]". Why is
> > the type variable translated to "Any"?
> >
> > Best,
> > Jan
>
> --
> Adam Gundry, Haskell Consultant
> Well-Typed LLP, http://www.well-typed.com/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20150302/faa46fb5/attachment-0001.html>