Opened 8 months ago
Last modified 7 days 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, #15635 | 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 (8)
comment:1 Changed 8 months ago by
Cc: | Iceland_jack added |
---|
comment:2 Changed 8 months ago by
comment:3 Changed 6 months ago by
Keywords: | wipT2893 removed |
---|
comment:4 Changed 2 weeks ago by
Related Tickets: | #14822 → #14822, #15635 |
---|
comment:6 Changed 2 weeks ago by
Here's a motivating example where I wish that I was able to show the compiler that one (quantified) constraint implies another. In this example, I'm using the singletons
library. The Data.Singletons.TypeLits
module contains
data instance Sing (n :: Nat) = KnownNat n => SNat instance KnownNat n => SingI n where sing = SNat
where the compiler learns of the implication forall n. KnownNat n => SingI n
. However the reverse implication forall n. SingI n => KnownNat n
is also true as evidenced by:
data Dict :: Constraint -> Type where Dict :: c => Dict c singIToKnownNat :: forall n. SingI n => Dict (KnownNat n) singIToKnownNat = case sing @n of SNat -> Dict
The crux is that there's is no way to rephrase singIToKnownNat
in terms of constraint implication:
singIImpliesKnownNat :: forall r. ((forall n. SingI n => KnownNat n) => r) -> r singIImpliesKnownNat a = undefined -- Can't implement this?
What this ticket asks for is some way to write a correct definition of things like singIImpliesKnownNat
. Something similar to the definition of singIToKnownNat
, I would imagine.
Here's the full example code:
-- GHC 8.6.2, Singletons 2.5 {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE QuantifiedConstraints #-} module ReifyImplications where import Data.Kind import GHC.TypeNats import Data.Singletons import Data.Singletons.TypeLits import Data.Type.Equality data EmptyVec :: Nat -> Type where EmptyVec :: EmptyVec 0 instance KnownNat n => Read (EmptyVec n) where readsPrec _ "EmptyVec" = case sameNat @n @0 Proxy Proxy of Just Refl -> [(EmptyVec, "")] Nothing -> [] data Some1 :: (k -> Type) -> Type where Some1 :: Sing a -> f a -> Some1 f readKnowingTypeIndex :: forall k (f :: k -> Type). (forall x. SingI x => Read (f x)) => SomeSing k -> String -> Some1 f readKnowingTypeIndex (SomeSing s) str = Some1 s $ withSingI s $ read str readKnowingNat :: forall (f :: Nat -> Type). (forall n. KnownNat n => Read (f n)) => SomeSing Nat -> String -> Some1 f readKnowingNat (SomeSing (SNat :: Sing a)) str = Some1 (SNat @a) $ read str -- Can't write this in terms of readKnowingTypeIndex? ev :: SomeSing Nat -> Some1 EmptyVec --ev s = readKnowingTypeIndex s "EmptyVec" -- Could not deduce (KnownNat x). --ev s = readKnowingNat s "EmptyVec" -- OK, but this doesn't work on every kind. Only Nat. singIImpliesKnownNat :: forall r. ((forall n. SingI n => KnownNat n) => r) -> r singIImpliesKnownNat a = undefined -- Can't implement this? ev s = singIImpliesKnownNat $ readKnowingTypeIndex s "EmptyVec" -- OK, if singIImpliesKnownNat was real. -- Now, this is easy to implement. But it's not practically usable in the definition of `ev`. data Dict :: Constraint -> Type where Dict :: c => Dict c singIToKnownNat :: forall n. SingI n => Dict (KnownNat n) singIToKnownNat = case sing @n of SNat -> Dict -- Bonus: readKnowingNat written in terms of readKnowingTypeIndex readKnowingNat' :: forall (f :: Nat -> Type). (forall n. KnownNat n => Read (f n)) => SomeSing Nat -> String -> Some1 f readKnowingNat' s str = singIImpliesKnownNat $ readKnowingTypeIndex s str
comment:7 Changed 2 weeks ago by
I end up wishing that I could put myself in some sort of context where I claim that "n
could be anything, and suppose we have SingI n
", so that I'm allowed to call singIToKnownNat @n
. In this context, the fact that we're able to produce a Dict (KnownNat n)
, should prove to the compiler that forall n. SingI n => KnownNat n
.
The expression that you provide in this context would get implicitly pattern matched, in order to learn the constraints that can result from the assumption made in the context. The compiler concludes that the assumed constraint implies the constraints found by the implicit pattern match.
I'll make up some syntax for this. Imagine a suppose ... in ...
keyword:
ev :: SomeSing Nat -> Some1 EmptyVec ev s = suppose forall (n :: Nat). SingI n => singIToKnownNat @n in readKnowingTypeIndex s "EmptyVec"
It's a funny mix of type level and expression level syntax. singIToKnownNat @n
soundly returns a Dict (KnownNat n)
, and pattern matching on the resulting Dict
constructor would make us learn that for all n
, SingI n
(from the suppose
context) implies KnownNat n
.
In fact this has nothing to do with Dict
. The following would work equally well:
ev :: SomeSing Nat -> Some1 EmptyVec ev s = suppose forall (n :: Nat). SingI n => sing @n in readKnowingTypeIndex s "EmptyVec"
since, after all, sing @n
returns an SNat :: Sing n
, which when pattern matched brings KnownNat n
into scope.
I don't mean to pollute language syntax. If there's a way to avoid new syntax, like a magical built-in function, that's preferable. It also has to be able to quantify over various numbers of type variables, so I don't think the built-in function that I proposed in the description would even work in this practical case.
I'm a bit curious. When I try to write
suppose1 :: forall a b r. (forall x. a x => Dict (b x)) -> ((forall x. a x => b x) => r) -> r suppose1 Dict a = a
GHC complains already on the type signature: Could not deduce: b x
. What's going on there?
I wouldn't be surprised if it's already possible today to write something magical using unsafeCoerce that works for specific cases, in the style of Edward Kmett's reflection
package. But that's not a long-term solution.
comment:8 Changed 2 weeks ago by
I just realized that the "implicit pattern match" is nonsense, as it's not indicated at compile time which constructor the pattern match resulted in.
So something more like:
ev :: SomeSing Nat -> Some1 EmptyVec ev s = case forall n. SingI n => sing @n of SNat -> -- Constraint brought into scope: (forall n. SingI n => KnownNat n) readKnowingTypeIndex s "EmptyVec"
Also makes it clear that the expression is being evaluated.
See also #14832