[GHC] #14937: QuantifiedConstraints: Reify implication constraints from terms lacking them
#14937: QuantifiedConstraints: Reify implication constraints from terms lacking them -------------------------------------+------------------------------------- Reporter: Bj0rn | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints, wipT2893 | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #14822 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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: {{{#!hs 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: {{{#!hs 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) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14937 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14937: QuantifiedConstraints: Reify implication constraints from terms lacking them -------------------------------------+------------------------------------- Reporter: Bj0rn | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints, wipT2893 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: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14937#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14937: QuantifiedConstraints: Reify implication constraints from terms lacking them -------------------------------------+------------------------------------- Reporter: Bj0rn | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints, wipT2893 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: | -------------------------------------+------------------------------------- Comment (by simonpj): See also #14832 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14937#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14937: QuantifiedConstraints: Reify implication constraints from terms lacking them -------------------------------------+------------------------------------- Reporter: Bj0rn | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints 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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: QuantifiedConstraints, wipT2893 => QuantifiedConstraints -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14937#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14937: QuantifiedConstraints: Reify implication constraints from terms lacking them -------------------------------------+------------------------------------- Reporter: Bj0rn | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints 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: | -------------------------------------+------------------------------------- Changes (by Bj0rn): * related: #14822 => #14822, #15635 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14937#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14937: QuantifiedConstraints: Reify implication constraints from terms lacking them -------------------------------------+------------------------------------- Reporter: Bj0rn | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints 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: | -------------------------------------+------------------------------------- Comment (by Bj0rn): #15635 Describes the same problem, perhaps in a clearer way. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14937#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14937: QuantifiedConstraints: Reify implication constraints from terms lacking them -------------------------------------+------------------------------------- Reporter: Bj0rn | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints 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: | -------------------------------------+------------------------------------- Comment (by Bj0rn): 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 {{{#!hs 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: {{{#!hs 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: {{{#!hs 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: {{{#!hs -- 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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14937#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14937: QuantifiedConstraints: Reify implication constraints from terms lacking them -------------------------------------+------------------------------------- Reporter: Bj0rn | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints 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: | -------------------------------------+------------------------------------- Comment (by Bj0rn): 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: {{{#!hs 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: {{{#!hs 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 {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14937#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14937: QuantifiedConstraints: Reify implication constraints from terms lacking them -------------------------------------+------------------------------------- Reporter: Bj0rn | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints 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: | -------------------------------------+------------------------------------- Comment (by Bj0rn): 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: {{{#!hs ev :: SomeSing Nat -> Some1 EmptyVec ev s = case forall (n :: Nat). SingI n => singIToKnownNat @n of Dict -> readKnowingTypeIndex s "EmptyVec" }}} Also makes it clear that the expression is being evaluated. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14937#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14937: QuantifiedConstraints: Reify implication constraints from terms lacking them -------------------------------------+------------------------------------- Reporter: Bj0rn | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints 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: | -------------------------------------+------------------------------------- Changes (by dfeuer): * cc: dfeuer (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14937#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14937: QuantifiedConstraints: Reify implication constraints from terms lacking them -------------------------------------+------------------------------------- Reporter: Bj0rn | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints 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: | -------------------------------------+------------------------------------- Comment (by dfeuer): The magical built-in function doesn't seem like strong enough medicine. Today, you asked for {{{#!hs reifyImplication :: forall a b. (forall r. a => (b => r) -> r) -> (forall r. ((a => b) => r) -> r) }}} But tomorrow, you might need {{{#!hs reifyImplication1 :: forall a b. (forall r x. a x => (b x => r) -> r) -> (forall r. ((forall x. a x => b x) => r) -> r) reifyImplication2 :: forall a b. (forall r x y. a x y => (b x y => r) -> r) -> (forall r. ((forall x y. a x y => b x y) => r) -> r) }}} and the day after that, you may want {{{#!hs reifyImplicationQ :: forall a b y. (forall r x. a x y => (b x y => r) -> r) -> (forall r. ((forall x. a x y => b x y) => r) -> r) }}} and so on. It would be possible to offer a whole set of these primitives, but it would be a bit of a mess and never complete. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14937#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC