Fwd: EvTerms and how they are used
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
2015-02-25 13:35 GMT+00:00 Adam Gundry
Hi Jan,
Yes, unfortunately the meaning of EvTerm is a weak point of the current typechecker plugins story; it rather requires one to understand how GHC's constraint solver produces evidence. There are lots of papers on evidence for equality constraints in System FC, but typeclass constraints are generally ignored as they are just datatypes at the FC level.
Let me try to give you some idea of what EvDFunApp means, then hopefully those with more knowledge of the GHC internals can correct me...
If you write a class instance, e.g.
instance (Show a, Show b) => Show (T a b) where ...
then GHC generates a dfun (short for "dictionary function", I guess)
$fShowT :: forall a b . (Show a, Show b) => Show (T a b)
where Show is treated as a record data type containing a dictionary of methods for the class. At the core level, this is a normal term-level function (albeit with a strange name).
Now when the typechecker has a constraint to solve, say
Show (T Int Bool),
it produces evidence for this by applying $fShowT to the appropriate types and to evidence for the superclass constraints, in this case something like
$fShowT @Int @Bool $fShowInt $fShowBool
where I'm using @ for type application. This is represented in EvTerm as
EvDFunApp $fShowT [Int, Bool] [ EvDFunApp $fShowInt [] [] , EvDFunApp $fShowBool [] [] ]
Thus the [Type] is the list of kinds/types at which to instantiate the dfun, and the [EvTerm] is the list of evidence terms to which it must be applied. Obviously this application should be well-typed, and -dcore-lint will complain if it is not.
For typechecker plugins, it would be nice if we could write arbitrary core expressions as evidence, but this hasn't yet been implemented (partially because most of the examples so far solve equality constraints, rather than typeclass constraints).
Hope this helps,
Adam
On 25/02/15 10:55, Jan Bracker wrote:
Hello,
I am trying to use the new type checker plugins [1] that are implemented in head.
When successful a plugin has to return a [(EvTerm, Ct)] for the solved constraints. The documentation on EvTerms is scarce [2,3,4] and I could not find papers that explain them (many talk about 'evidence', but they never get concrete).
So far I have figured out that "EvDFunApp DFunId [Type] [EvTerm]" selects a certain instance to be used for a constraint, though I don't know what the list of EvTerms in the end is for. I am also a bit unclear on how the "[Type]" is used.If I turn on '-dcore-lint' I get errors. So I still seem to be using it wrong.
I have also asked in IRC, but did not get a response to my question.
I am sorry if this is the wrong mailing list to ask. If there is a more apropriate place just point it out.
Best, Jan
[1]: https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker [2]: http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/libraries/ghc-7.1... [3]: http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/libraries/ghc-7.1... [4]: http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/users_guide/compi...
-- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/
Hi Jan, 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. <digression>The `Any` type is used by GHC to instantiate type variables whose values are irrelevant, because they do not occur in the type. The classic example is `null []`, where the type of the list is unimportant: rather than having an unsolved unification variable, GHC solves it with `Any`.</digression> 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)? 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! Emitting this extra derived constraint is essentially what happens if you specify the functional dependency class Polymonad m n p | m p -> n where but the plugin approach allows more fine-grained control over exactly when this applies. 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. All the best, Adam 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/
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/
Hello,
I've seen instances of this problem show up over and over again, and I
think that there is a more principled solution, based on the idea of
`improvement`.
The idea is to allow programmers to specify custom improvements.
Functional dependencies are one way to do this, but there is no reason why
this
should be the only way. The details of this idea are explained in this
paper: "Simplifying and Improving Qualified Types" (
http://web.cecs.pdx.edu/~mpj/pubs/RR-1040.pdf).
In concrete Haskell syntax, this might work like this:
1. Add a new declaration:
improve CS using EQs
Here the `CS` are a collection of constraints, and the `EQs` are a
collection of equations.
2. Modify the constraint solver, so that when it sees `CS` in the inert
set, it will emit the `EQs` as derived constraints.
This is all.
So now you can write things like this:
improve PolyMonad a b Identity using (a ~ Identity, b ~ Identity)
This tells GHC that it is OK to assume that if the final result is
`Identity`,
then the first two arguments will also be in the identity monad.
This is a fairly conservative extension, in that it is only used to
instantiate variables,
and it never needs to produce new equality proofs. This is pretty much
exactly how FDs work
in the current implementation of GHC. For example, the declaration:
class C a b | a -> b where ...
with GHC's current implementation, is exactly equivalent to:
class C a b where ...
improve (C a b, C a c) using (b ~ c)
Aside: GHC actually checks that all instances are consistent with the FD
declarations,
so GHC *could* use them to actually generate new evidence, but it does not
do so at the moment.
Anyway, implementing something like this should not be too hard, and it
seems that it could be
used not just for the PolyMonads work, but also for other cases where one
wants to write
specific improvements.
-Iavor
PS: with GHC's current approach to resolving instances, you could also
avoid some of the
ambiguities for the `Identity` instance by writing it like this:
instance (a ~ Identity, b ~ Idnetity) => PolyMonad a b Identity where
...
On Mon, Mar 2, 2015 at 8:38 AM, 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/
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
participants (3)
-
Adam Gundry -
Iavor Diatchki -
Jan Bracker