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 Iceland_jack

Cc: Iceland_jack added

comment:2 Changed 4 months ago by simonpj

See also #14832

comment:3 Changed 7 weeks ago by RyanGlScott

Keywords: wipT2893 removed
Note: See TracTickets for help on using tickets.