# Implementation details are needed for proofs #339

Open
opened this Issue Jun 13, 2018 · 5 comments

Projects
None yet
3 participants
Contributor

### howtonotwin commented Jun 13, 2018 • edited

 A proof about a function needs to have the implementation details of the function. In `singletons`, functions are type families, and type families must expose all their equations (AKA their implementation). However, functions that use `let`/`where` create helper type families, where the implementation is known, but the type families themselves have unutterable names. It becomes impossible to write proofs for these hidden functions, so proofs for the whole function become impossible. E.g. ```\$(singletons [d| data Nat = Z | S Nat add :: Nat -> Nat -> Nat add Z r = r add (S l) r = S (add l r) |]) data IsS (n :: Nat) where IsS :: IsS (S n) {- we already have (from Data.Singletons.Prelude) \$(singletons [d| foldr :: (a -> b -> b) -> b -> [a] -> b foldr k n = go where go [] = n go (x:xs) = x `k` go xs |]) -} -- Is provable given more Sing arguments; but this version is nicer to use. addIsS :: Either (IsS l) (IsS r) -> IsS (Add l r) addIsS _ = unsafeCoerce IsS data Elem (x :: k) (xs :: [k]) where Here :: Elem x (x : xs) There :: Elem x xs -> Elem x (y : xs) data Exists (pred :: k ~> Type) (xs :: [k]) = forall (x :: k). Exists (Elem x xs) (pred @@ x) -- problem here sumIsS :: forall xs. Exists (TyCon IsS) xs -> IsS (Foldr AddSym0 Z xs) sumIsS (Exists Here prf) = addIsS @(Head xs) @(Foldr AddSym0 Z (Tail xs)) (Left prf) sumIsS (Exists (There i) prf) = addIsS @(Head xs) @(Foldr AddSym0 Z (Tail xs)) (Right (sumIsS (Exists i prf)))``` Both cases fail with a similar error ``````Could not deduce: Add y (Data.Singletons.Prelude.Base.Let6989586621679697830Go AddSym0 'Z xs1 xs1) ~ Add y (Data.Singletons.Prelude.Base.Let6989586621679697830Go AddSym0 'Z (y : xs1) xs1) `````` The issue is that the `go` in `foldr`, when promoted, gets an (unused) argument that represents `foldr`'s list argument. This mucks up the proof, where it isn't clear that the argument doesn't matter. Because this function has no stable name, not to mention its unexported status, one can't prove around that. It seems impossible to write `sumIs`. I feel like a fix for this deserves to be in `singletons`. Here are a couple ways: Remove `go` from `foldr`. Replacing `foldr` with a nicer version fixes this: ```\$(singletonsOnly [d| foldr' _ n [] = n foldr' k n (x:xs) = x `k` foldr' k n xs |]) sumIsS :: forall xs. Exists (TyCon IsS) xs -> IsS (Foldr' AddSym0 Z xs) sumIsS (Exists Here prf) = addIsS @(Head xs) @(Foldr' AddSym0 Z (Tail xs)) (Left prf) sumIsS (Exists (There i) prf) = addIsS @(Head xs) @(Foldr' AddSym0 Z (Tail xs)) (Right (sumIsS (Exists i prf)))``` I think, sometimes, this strategy will fail. In those cases, the helper function can be wholly lifted out. However, this is a complicated procedure. Further, the changes involved are to the functions being promoted themselves. This requires actual effort by the person writing the functions (i.e. me), which is at odds to the fact that I am lazy. If the promoted functions in `singletons` were changed like this, I also think maintainability would take a hit, due to the changes to the `base` code `singletons` copies. Expose the implementation details of promoted functions. Give stable names to all the supporting definitions for a promoted function, which lets them be exported and talked about. This kicks the number of things that can appear in export lists from "high" to "higher" (further evidence for TH-controlled exports). This also has the effect of coupling (even further than usual) the API of a promoted function to the exact way `singletons` decides to promote it. I'm not sure what the stance is on that, or even how fast `singletons`'s implementation changes currently. There's always the option of making only some things stable (e.g. `where` clauses get stable names, `case`s don't, etc.).
Owner

### goldfirere commented Jun 14, 2018

 What you want is reasonable. And perhaps key functions, like `foldr`, can be rewritten as you suggest. But part of the point of `singletons` is so that you don't have to rewrite your functions! Yet, option (2) seems terrible and fragile. Maybe the solution is for lambda-lifting to be a bit cleverer in its approach. We could likely tell statically that we don't need `foldr`'s last argument and so can leave it off when lifting. That will solve your immediate problem, but perhaps we can settle for that, for now.

Collaborator

### RyanGlScott commented Jun 14, 2018

 Indeed, lambda-lifting of local functions is quite un-optimized at the moment and always captures all variables that are in scope at the definition site, even if they are not actually free in the definition itself. A conceptually simple fix would be to implement a function which computes the free variables of a definition and only capture those variables when we lift a closure to the top level during promotion. (In your particular example, this means that the promoted version of `go` would only capture `k`.) `th-desugar` would be a good place to put this function, as it already has the ability to compute the free variables of types (here). We would just need a term-level counterpart as well.
Owner

### goldfirere commented Jun 14, 2018

 Yes, that's just what I was thinking, if you wanted to implement it. :)
Collaborator

### RyanGlScott commented Jul 5, 2018

It looks like this problem will strike in more places in the upcoming `singletons-2.5` release. For example, this code typechecks with `singletons-2.4`:

```{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Kind
import Data.Singletons.Prelude
import Data.Singletons.TH

\$(singletons [d|
forallb :: (a -> Bool) -> [a] -> Bool
forallb = all

existsb, existsb' :: (a -> Bool) -> [a] -> Bool
existsb = any
existsb' p = not . forallb (not . p)
|])

existsbExistsb' :: forall (a :: Type) (p :: a ~> Bool) (l :: [a]).
Sing p -> Sing l
-> Existsb' p l :~: Existsb p l
existsbExistsb' _  SNil = Refl
existsbExistsb' sp (SCons sx sls)
= case sp @@ sx of
STrue -> Refl
SFalse
| Refl <- existsbExistsb' sp sls
-> Refl```

But not with `singletons-2.5`:

``````../../Bug.hs:29:16: error:
• Could not deduce: Not
(Data.Singletons.Prelude.Foldable.Case_6989586621680649554
(NotSym0 .@#@\$\$\$ p)
(n1 : n2)
(singletons-2.5:Data.Singletons.Prelude.Semigroup.Internal.TFHelper_6989586621680181224
('base-4.12.0.0:Data.Semigroup.Internal.All 'False)
(Data.Singletons.Prelude.Base.Let6989586621679917966Go
(MappendSym0
.@#@\$\$\$ (singletons-2.5:Data.Singletons.Prelude.Semigroup.Internal.All_Sym0
.@#@\$\$\$ (NotSym0 .@#@\$\$\$ p)))
('base-4.12.0.0:Data.Semigroup.Internal.All 'True)
(n1 : n2)
n2)))
~ Data.Singletons.Prelude.Foldable.Case_6989586621680649567
p
(n1 : n2)
(singletons-2.5:Data.Singletons.Prelude.Semigroup.Internal.TFHelper_6989586621680181236
('base-4.12.0.0:Data.Semigroup.Internal.Any 'True)
(Data.Singletons.Prelude.Base.Let6989586621679917966Go
(MappendSym0
.@#@\$\$\$ (singletons-2.5:Data.Singletons.Prelude.Semigroup.Internal.Any_Sym0
.@#@\$\$\$ p))
('base-4.12.0.0:Data.Semigroup.Internal.Any 'False)
(n1 : n2)
n2))
from the context: l ~ (n1 : n2)
bound by a pattern with constructor:
SCons :: forall a (n1 :: a) (n2 :: [a]).
Sing n1 -> Sing n2 -> Sing (n1 : n2),
in an equation for ‘existsbExistsb'’
at ../../Bug.hs:27:21-32
or from: Apply p n1 ~ 'True
bound by a pattern with constructor: STrue :: Sing 'True,
in a case alternative
at ../../Bug.hs:29:7-11
Expected type: Existsb' p l :~: Existsb p l
Actual type: Data.Singletons.Prelude.Foldable.Case_6989586621680649567
p
(n1 : n2)
(singletons-2.5:Data.Singletons.Prelude.Semigroup.Internal.TFHelper_6989586621680181236
('base-4.12.0.0:Data.Semigroup.Internal.Any 'True)
(Data.Singletons.Prelude.Base.Let6989586621679917966Go
(MappendSym0
.@#@\$\$\$ (singletons-2.5:Data.Singletons.Prelude.Semigroup.Internal.Any_Sym0
.@#@\$\$\$ p))
('base-4.12.0.0:Data.Semigroup.Internal.Any 'False)
(n1 : n2)
n2))
:~: Data.Singletons.Prelude.Foldable.Case_6989586621680649567
p
(n1 : n2)
(singletons-2.5:Data.Singletons.Prelude.Semigroup.Internal.TFHelper_6989586621680181236
('base-4.12.0.0:Data.Semigroup.Internal.Any 'True)
(Data.Singletons.Prelude.Base.Let6989586621679917966Go
(MappendSym0
.@#@\$\$\$ (singletons-2.5:Data.Singletons.Prelude.Semigroup.Internal.Any_Sym0
.@#@\$\$\$ p))
('base-4.12.0.0:Data.Semigroup.Internal.Any 'False)
(n1 : n2)
n2))
• In the expression: Refl
In a case alternative: STrue -> Refl
In the expression:
case sp @@ sx of
STrue -> Refl
SFalse | Refl <- existsbExistsb' sp sls -> Refl
• Relevant bindings include
sls :: Sing n2 (bound at ../../Bug.hs:27:30)
sx :: Sing n1 (bound at ../../Bug.hs:27:27)
sp :: Sing p (bound at ../../Bug.hs:27:17)
existsbExistsb' :: Sing p -> Sing l -> Existsb' p l :~: Existsb p l
(bound at ../../Bug.hs:26:1)
|
29 |       STrue -> Refl
|                ^^^^

../../Bug.hs:32:12: error:
• Could not deduce: Not
(Data.Singletons.Prelude.Foldable.Case_6989586621680649554
(NotSym0 .@#@\$\$\$ p)
(n1 : n2)
(singletons-2.5:Data.Singletons.Prelude.Semigroup.Internal.TFHelper_6989586621680181224
('base-4.12.0.0:Data.Semigroup.Internal.All 'True)
(Data.Singletons.Prelude.Base.Let6989586621679917966Go
(MappendSym0
.@#@\$\$\$ (singletons-2.5:Data.Singletons.Prelude.Semigroup.Internal.All_Sym0
.@#@\$\$\$ (NotSym0 .@#@\$\$\$ p)))
('base-4.12.0.0:Data.Semigroup.Internal.All 'True)
(n1 : n2)
n2)))
~ Data.Singletons.Prelude.Foldable.Case_6989586621680649567
p
(n1 : n2)
(singletons-2.5:Data.Singletons.Prelude.Semigroup.Internal.TFHelper_6989586621680181236
('base-4.12.0.0:Data.Semigroup.Internal.Any 'False)
(Data.Singletons.Prelude.Base.Let6989586621679917966Go
(MappendSym0
.@#@\$\$\$ (singletons-2.5:Data.Singletons.Prelude.Semigroup.Internal.Any_Sym0
.@#@\$\$\$ p))
('base-4.12.0.0:Data.Semigroup.Internal.Any 'False)
(n1 : n2)
n2))
from the context: l ~ (n1 : n2)
bound by a pattern with constructor:
SCons :: forall a (n1 :: a) (n2 :: [a]).
Sing n1 -> Sing n2 -> Sing (n1 : n2),
in an equation for ‘existsbExistsb'’
at ../../Bug.hs:27:21-32
or from: Apply p n1 ~ 'False
bound by a pattern with constructor: SFalse :: Sing 'False,
in a case alternative
at ../../Bug.hs:30:7-12
or from: Existsb p n2 ~ Existsb' p n2
bound by a pattern with constructor:
Refl :: forall k (a :: k). a :~: a,
in a pattern binding in
pattern guard for
a case alternative
at ../../Bug.hs:31:11-14
Expected type: Existsb' p l :~: Existsb p l
Actual type: Data.Singletons.Prelude.Foldable.Case_6989586621680649567
p
(n1 : n2)
(singletons-2.5:Data.Singletons.Prelude.Semigroup.Internal.TFHelper_6989586621680181236
('base-4.12.0.0:Data.Semigroup.Internal.Any 'False)
(Data.Singletons.Prelude.Base.Let6989586621679917966Go
(MappendSym0
.@#@\$\$\$ (singletons-2.5:Data.Singletons.Prelude.Semigroup.Internal.Any_Sym0
.@#@\$\$\$ p))
('base-4.12.0.0:Data.Semigroup.Internal.Any 'False)
(n1 : n2)
n2))
:~: Data.Singletons.Prelude.Foldable.Case_6989586621680649567
p
(n1 : n2)
(singletons-2.5:Data.Singletons.Prelude.Semigroup.Internal.TFHelper_6989586621680181236
('base-4.12.0.0:Data.Semigroup.Internal.Any 'False)
(Data.Singletons.Prelude.Base.Let6989586621679917966Go
(MappendSym0
.@#@\$\$\$ (singletons-2.5:Data.Singletons.Prelude.Semigroup.Internal.Any_Sym0
.@#@\$\$\$ p))
('base-4.12.0.0:Data.Semigroup.Internal.Any 'False)
(n1 : n2)
n2))
• In the expression: Refl
In a case alternative:
SFalse | Refl <- existsbExistsb' sp sls -> Refl
In the expression:
case sp @@ sx of
STrue -> Refl
SFalse | Refl <- existsbExistsb' sp sls -> Refl
• Relevant bindings include
sls :: Sing n2 (bound at ../../Bug.hs:27:30)
sx :: Sing n1 (bound at ../../Bug.hs:27:27)
sp :: Sing p (bound at ../../Bug.hs:27:17)
existsbExistsb' :: Sing p -> Sing l -> Existsb' p l :~: Existsb p l
(bound at ../../Bug.hs:26:1)
|
32 |         -> Refl
|            ^^^^
``````

The culprit is that I changed the definition of `all` from this (in `singletons-2.4`):

Lines 359 to 361 in 8aeba2a

 all :: (a -> Bool) -> [a] -> Bool all _ [] = True all p (x:xs) = p x && all p xs

To this (in `singletons-2.5`):

Lines 600 to 602 in 60dd52c

 all :: Foldable t => (a -> Bool) -> t a -> Bool all p x = case foldMap (all_ . p) x of Monoid.All y -> y

Just like the issue with `foldr`, I believe that making `singletons` close over fewer variables when lambda lifting would be sufficient to fix this buglet.

Collaborator

### RyanGlScott commented Sep 19, 2018 • edited

 For any readers out there who are interested in fixing this bug, I've just pushed a `FVs` branch in `th-desugar` which adds a plethora of new functions that compute free variables. It's my hope that these will be useful in implementing the suggestion in #339 (comment). Edit: The `FVs` branch has been merged into `master`.

Merged

Open