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 Iceland_jack

Cc: Iceland_jack added

comment:2 Changed 8 months ago by simonpj

See also #14832

comment:3 Changed 6 months ago by RyanGlScott

Keywords: wipT2893 removed

comment:4 Changed 2 weeks ago by Bj0rn

comment:5 Changed 2 weeks ago by Bj0rn

#15635 Describes the same problem, perhaps in a clearer way.

comment:6 Changed 2 weeks ago 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

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 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:

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 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:

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.

Last edited 7 days ago by Bj0rn (previous) (diff)
Note: See TracTickets for help on using tickets.