Opened 4 months ago
Last modified 7 weeks ago
#14937 new feature request
QuantifiedConstraints: Reify implication constraints from terms lacking them
Reported by: | Bj0rn | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.5 |
Keywords: | QuantifiedConstraints | Cc: | Iceland_jack |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #14822 | Differential Rev(s): | |
Wiki Page: |
Description
This is possibly the same question as #14822, asked in more general terms. Would it be viable/sound to have a way of extracting implication constraints out of terms which effectively encode such constraints, such as (:-)
from Data.Constraint
?
Here's how I think about it. a :- b
is equivalent to forall r. a => (b => r) -> r
. This is a type that, as I read it, expresses "if you can show a
, then I can show b
". This is very similar to forall r. ((a => b) => r) -> r
, which expresses "(without obligations) I can show that a
implies b
".
It seems to me (and I know this is hand-wavy) like expressions of both of these types actually must have the same "knowledge", i.e. that a
imples b
. Is this actually correct?
I am wondering whether we could have a built-in function like:
reifyImplication :: forall a b. (forall r. a => (b => r) -> r) -> (forall r. ((a => b) => r) -> r)
We can already write the function that goes the other direction.
There are plenty of ways to represent this conversion. Some more straight-forward, using a :- b
or Dict a -> Dict b
. I just went with one that doesn't require any types beyond arrows.
I'm curious about the soundness of this. I have tried really hard to implement this function, but I don't think it can be done.
I don't know if this proves anything, but replacing (=>)
with (->)
and all constraints c
with Dict c
, this function can be written:
dictReifyImplication :: forall a b. (forall r. Dict a -> (Dict b -> r) -> r) -> (forall r. ((Dict a -> Dict b) -> r) -> r) dictReifyImplication f g = g (\a -> f a id)
Change History (3)
comment:1 Changed 4 months ago by
Cc: | Iceland_jack added |
---|
comment:2 Changed 4 months ago by
comment:3 Changed 7 weeks ago by
Keywords: | wipT2893 removed |
---|
See also #14832