Opened 12 months ago
Closed 10 months ago
#15635 closed feature request (duplicate)
Implication introduction for quantified constraints
Reported by: | dfeuer | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.6.1 |
Component: | Compiler | Version: | 8.6.1-beta1 |
Keywords: | QuantifiedConstraints | Cc: | Bj0rn |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #14937 | Differential Rev(s): | |
Wiki Page: |
Description
Now that we have QuantifiedConstraints
, it seems we need some implication introduction form. The constraints
package has these types:
data Dict a where Dict :: a => Dict a newtype a :- b = Sub (a => Dict b)
QuantifiedConstraints
suggests another version of :-
:
newtype Imp a b = Imp { unImp :: forall r. ((a => b) => r) -> r}
We can write
fromImp :: Imp a b -> a :- b fromImp (Imp f) = Sub (f Dict)
But ... there's no way to go the other way!
Let's try it:
toImp :: a :- Dict b -> a :- b toImp (Sub ab) = Imp $ \r -> _
We get
* Found hole: _ :: r * Relevant bindings include r :: (a => b) => r ab :: a => Dict b
There's no way to put these things together. But there's no terribly obvious reason they can't be combined. a => b
is a function from an a
dictionary to a b
dictionary. a => Dict b
is a function from an a
dictionary to a value that contains a b
dictionary. We just need some way to plumb these things together: some sort of implication introduction. The simplest thing might be a bit of magic:
implIntro :: ((a => b) => q) -> (forall r. (b => r) -> (a => r)) -> q
In Core (modulo type abstraction and application), we could simply write
implIntro f g = f (g id)
Unfortunately, I doubt that implIntro
is really general enough to do everything people will want in this space.
Change History (3)
comment:1 Changed 10 months ago by
comment:2 Changed 10 months ago by
Cc: | Bj0rn added |
---|---|
Related Tickets: | → #14937 |
comment:3 Changed 10 months ago by
Resolution: | → duplicate |
---|---|
Status: | new → closed |
This is the same as #14937.