singletons
singletons copied to clipboard
goldfirere
Implementation details are needed for proofs
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
gofromfoldr. Replacingfoldrwith 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
singletonswere changed like this, I also think maintainability would take a hit, due to the changes to thebasecodesingletonscopies. -
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
singletonsdecides to promote it. I'm not sure what the stance is on that, or even how fastsingletons's implementation changes currently. There's always the option of making only some things stable (e.g.whereclauses get stable names,cases don't, etc.).
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.
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.
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 TemplateHaskell #-}
{-# 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):
https://github.com/goldfirere/singletons/blob/8aeba2abedb21a67303def14c650d9a4a808162e/src/Data/Singletons/Prelude/List.hs#L359-L361
To this (in singletons-2.5):
https://github.com/goldfirere/singletons/blob/60dd52ccb725f966df4e34499023aca8a9b6974d/src/Data/Singletons/Prelude/Foldable.hs#L600-L602
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.
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 https://github.com/goldfirere/singletons/issues/339#issuecomment-397309205.
Edit: The FVs branch has been merged into master.
Another example, related to ZipWith:
-- Example 0, needs unsafeCoerce
withLookupKV0
:: forall (k :: kt) kk vv r
. SEq kt
=> KVList (kk :: [kt]) vv
-> Sing k
-> KVList (kk :: [kt]) (Fmap (FlipSym2 (TyCon2 (->)) r) vv)
-> Maybe r
withLookupKV0 tab k conts = case hLookupKV k tab of
TNothing -> Nothing
TJust v -> case hLookupKV k conts of
TNothing -> Nothing
TJust cont -> Just ((unsafeCoerce cont) v)
-- without unsafeCoerce, GHC "Could not deduce: t1 ~ (t -> r)"
OK, let's try zipping together the lists first, to hopefully keep the related type information together, maybe that helps the typechecker:
-- helper function
zipKV :: KVList kk v1 -> KVList kk v2 -> KVList kk (ZipWith (TyCon (,)) v1 v2)
zipKV KVNil KVNil = KVNil
zipKV (KVCons k v1 vv1) (KVCons _ v2 vv2) = KVCons k (v1, v2) (zipKV vv1 vv2)
-- Example 1, needs unsafeCoerce
withLookupKV
:: forall (k :: kt) kk vv r
. SEq kt
=> KVList (kk :: [kt]) vv
-> Sing k
-> KVList (kk :: [kt]) (Fmap (FlipSym2 (TyCon2 (->)) r) vv)
-> Maybe r
withLookupKV tab k conts = case hLookupKV k (zipKV tab conts) of
TNothing -> Nothing
TJust x -> let (v, cont) = unsafeCoerce x in Just (cont v)
-- without unsafeCoerce, GHC "Could not deduce: t ~ (t0, t0 -> r)"
OK, let's try explicit recursion that hopefully gives us access to the types like how we did in hLookupKV back in #447:
-- Example 2, needs unsafeCoerce
withLookupKV'
:: forall (k :: kt) kk vv r
. SEq kt
=> KVList (kk :: [kt]) vv
-> Sing k
-> KVList (kk :: [kt]) (Fmap (FlipSym2 (TyCon2 (->)) r) vv)
-> Maybe r
withLookupKV' tab k conts = go (Proxy @vv) (zipKV tab conts)
where
go
:: forall kk vv r
. Proxy vv
-> KVList (kk :: [kt]) (ZipWith (TyCon (,)) vv (Fmap (FlipSym2 (TyCon2 (->)) r) vv))
-> Maybe r
go p KVNil = Nothing
go p (KVCons k' x (rem :: KVList kk' vv')) = case k %== k' of
STrue -> let (v, cont) = unsafeCoerce x in Just (cont v)
SFalse -> go (Proxy @vv') (unsafeCoerce rem)
-- also fails with "could not deduce" errors
-- apparently ZipWith is too complex for the type checker...
Let's try another explicit recursion, this time without zip:
-- Example 3, success, but non-compositional :(
withLookupKV''
:: forall (k :: kt) kk vv r
. SDecide kt
=> KVList (kk :: [kt]) vv
-> Sing k
-> KVList (kk :: [kt]) (Fmap (FlipSym2 (TyCon2 (->)) r) vv)
-> Maybe r
withLookupKV'' tab k conts = case (tab, conts) of
(KVNil, KVNil) -> Nothing
(KVCons k' v tab', KVCons _ ct conts') -> case k %~ k' of
Proved Refl -> Just (ct v)
Disproved d -> withLookupKV'' tab' k conts'
Yay, finally we did it, but we had to write the algorithm from scratch and our previous utility functions were useless :(
One consolation point however is that GHC seems able to reason with the Fmap (FlipSym2 (TyCon2 (->)) r) vv, it just fails with more complex expressions :(
Note: I wrote that last example 3 before I posted #447 so it still uses SDecide instead of SEq. It also works if you convert it to using SEq; both work fine without needing unsafeCoerce.
Another set of examples, this one relating to constraints instead of ZipWith:
unsafeCoerce doesn't help us here, it doesn't seem to help GHC resolve constraints (as far as I can tell anyway; I don't know how the type checker works in detail):
-- helper function, convert a list of constraints into a single constraint
type family ConstrainList (cc :: [Constraint]) :: Constraint where
ConstrainList '[] = ()
ConstrainList (c ': cc) = (c, ConstrainList cc)
-- Example 0, fails even with unsafeCoerce
lookupKVShow0
:: forall (k :: kt) kk vv
. SEq kt
=> ConstrainList (Fmap (TyCon Show) vv)
=> Sing k
-> KVList (kk :: [kt]) vv
-> Maybe String
lookupKVShow0 k tab = case hLookupKV k tab of
TNothing -> Nothing
TJust v -> Just (show (unsafeCoerce v)) -- "could not deduce (Show t)"
Luckily, we can implement it slightly differently with explicit recursion (as in the previous comment with ZipWith) and this works:
-- Example 1, success, but non-compositional :(
-- another lookup function explicitly designed to handle constraints
withCxtLookupKV
:: forall (k :: kt) kk vv cxt a
. SEq kt
=> ConstrainList (Fmap (TyCon cxt) vv)
=> Proxy cxt
-> Sing k
-> (forall v. cxt v => v -> a)
-> KVList (kk :: [kt]) vv
-> Maybe a
withCxtLookupKV p k ap = \case
KVNil -> Nothing
KVCons k' v tab -> case k %== k' of
STrue -> Just (ap v)
SFalse -> withCxtLookupKV p k ap tab
Now we can write the following:
-- consume the value directly
lookupKVShow
:: forall (k :: kt) kk vv
. SEq kt
=> ConstrainList (Fmap (TyCon Show) vv)
=> Sing k
-> KVList (kk :: [kt]) vv
-> Maybe String
lookupKVShow k = withCxtLookupKV (Proxy @Show) k show
-- or wrap it up and return it, for later consumption
-- | Some constrained value.
data SomeCxtVal c where
SomeCxtVal :: c v => !v -> SomeCxtVal c
lookupKVShow'
:: forall (k :: kt) kk vv
. SEq kt
=> ConstrainList (Fmap (TyCon Show) vv)
=> Sing k
-> KVList (kk :: [kt]) vv
-> Maybe (SomeCxtVal Show)
lookupKVShow' k = withCxtLookupKV (Proxy @Show) k SomeCxtVal
So, another phyrric victory, since we had to duplicate a utility function withCxtLookupKV from our original hLookupKV. Also note it maps a constraint over the values; if you want to map a constraint over the keys then you have to write another utility function. I tried writing a utility function that lets you map both which works, but you can't reuse it for the special cases where ether is empty - GHC seems unable to infer that ConstrainList (Fmap (TyCon EmptyConstraint) vv) is itself an empty constraint, unfortunately :(
All-in-all this experience in trying to write only-very-slightly-complex dependent code has been very frustrating, although I do appreciate that singletons has made parts of the process much easier, there is still a long way to go. The fact that things can work when you unroll all the compositions is both encouraging and discouraging at the same time.
I haven't examined your examples in close detail, but I don't think the issues you're experiencing are a symptom of this issue, which document unintended implementation details leaking through. As I mention in https://github.com/goldfirere/singletons/issues/447#issuecomment-612453185, there are some implementation details that are simply unavoidable when doing dependently typed programming. (Do correct me if I've misunderstood the nature of your examples.)
Admittedly I hadn't gotten around to actually attempting to write a proof when I posted those examples - I couldn't find examples of proofs or hints on how to write these anywhere. The example in the OP seems to be about encoding proofs as term-level functions, but I seem to rather need type-level constraints in my examples. I've now finally found an example by Stephanie Weirich, and made an attempt for my code.
The problem in my examples above ultimately stemmed from using the lookupKV function directly, and were solved by inlining it. So let's try to prove something about it, that can be used by the compiler at the caller's site. Our first goal is:
Fmap f (LookupKV k kk vv) ~ LookupKV k kk (Fmap f vv)
Trying it by hand, we could do something like this:
Inducting on kk vv:
Given:
Wf. (Fmap f (LookupKV k kk vv) ~ LookupKV k kk (Fmap f vv))
Sf. Just (Apply f v') ~ Fmap f (Just v')
Tf. Apply f v' ': Fmap f vv ~ Fmap f (v' ': vv)
Deduce:
(Fmap f (LookupKV k (k' ': kk) (v' ': vv)) ~ LookupKV k (k' ': kk) (Fmap f (v' ': vv)))
by (Tf), ~
LookupKV k (k' ': kk) (Apply f v' ': Fmap f vv)
Apply type-family reduction rule for LookupKV on both sides, which GHC knows...
if k == k' if k == k'
then -> Fmap f (Just v') by (Sf) ~ then -> Just (Apply f v')
else -> Fmap f (LookupKV k kk vv) by (Wf) ~ else -> Lookup k kk (Fmap f vv)
[].
OK so let's try it in the code:
{-# LANGUAGE ConstraintKinds, DataKinds, EmptyCase, FlexibleContexts, FlexibleInstances, GADTs,
LambdaCase, MultiParamTypeClasses, RankNTypes, PolyKinds, ScopedTypeVariables,
TemplateHaskell, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-}
import Data.Kind
import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Singletons.TypeLits
import Unsafe.Coerce (unsafeCoerce)
singletons [d|
lookupKV :: Eq k => k -> [k] -> [v] -> Maybe v
lookupKV k [] [] = Nothing
lookupKV k (k':kk) (v:vv) = if k == k' then Just v else lookupKV k kk vv
|]
-- Proof that (f v : fmap f vv) == (fmap f (v : vv))
class ((Apply f v ': Fmap f vv) ~ Fmap f (v ': vv))
=> Tf f v vv where
instance Tf f v vv
-- Trying an empty instance with no superclass "just in case"...
-- OK, GHC seems to already be able to deduce this itself,
-- so no need to write it explicitly.
-- Proof that Just (f v') == fmap f (Just v')
class (Just (Apply f v') ~ Fmap f (Just v')) => Sf f v'
instance Sf f v'
-- Again, GHC seems to already know this, given what's imported.
-- Proof that fmap f (lookupKV k kk vv) == lookupKV k kk (fmap f vv)
class (Fmap f (LookupKV k kk vv) ~ LookupKV k kk (Fmap f vv))
=> Wf f k (kk :: [kt]) vv where
instance
Wf f k '[] '[]
instance
(Wf f k kk vv, Vf f k k' kk v' vv (k == k'))
=> Wf f (k :: kt) (k' ': kk) (v' ': vv)
-- When we try to compile this without the constraint, GHC complains about
-- "could not deduce" something, so let's fill it in:
class (Fmap f (Case_6989586621679077040 k k' kk v' vv eq) ~
Case_6989586621679077040 k k' kk (Apply f v') (Fmap f vv) eq)
=> Vf f (k :: kt) k' kk v' vv eq where
instance Vf f k k' kk v' vv 'True
-- ^ as per our paper proof, this does not require Wf, but only Sf which GHC knows for free
instance (Wf f k kk vv) => Vf f k k' kk v' vv 'False
-- ^ the real inductive step
-------------------------------------------------------------------------------
-- Heterogeneous map implementation
-- heterogeneous Maybe that carries the type
data TMaybe (t :: Maybe k) where
TNothing :: TMaybe 'Nothing
TJust :: !t -> TMaybe ('Just t)
data KVList (kk :: [kt]) (vv :: [Type]) :: Type where
KVNil :: KVList '[] '[]
KVCons :: !(Sing (k :: kt)) -> !(v :: Type) -> !(KVList kk vv) -> KVList (k : kk) (v : vv)
hLookupKV
:: SEq kt
=> Sing (k :: kt)
-> KVList (kk :: [kt]) vv
-> TMaybe (LookupKV k kk vv)
hLookupKV sk KVNil = TNothing
hLookupKV sk (KVCons sk'' v rem) = case sk %== sk'' of
STrue -> TJust v
SFalse -> hLookupKV sk rem
-- Example 0, failing before
withLookupKV0
:: forall (k :: kt) kk vv r
. SEq kt
=> Wf (FlipSym2 (TyCon2 (->)) r) k kk vv -- this constraint makes the deduction go through, yay!
=> KVList (kk :: [kt]) vv
-> Sing k
-> KVList (kk :: [kt]) (Fmap (FlipSym2 (TyCon2 (->)) r) vv)
-> Maybe r
withLookupKV0 tab k conts = case hLookupKV k tab of
TNothing -> Nothing
TJust v -> case hLookupKV k conts of
TNothing -> Nothing
-- ^ nice, GHC even warns us about "inaccessible right hand side" since we
-- already performed the same lookup previously
TJust cont -> Just (cont v)
main = do
let v = KVCons (SSym @"a") (3 :: Int) $ KVCons (SSym @"b") "test" $ KVNil
let c = KVCons (SSym @"a") (show . (+ (2 :: Int))) $ KVCons (SSym @"b") (<> "ing") $ KVNil
-- great, this compiles, GHC can deduce `Wf` and `Vf` automatically from concrete examples
case withLookupKV0 v (SSym @"a") c of
Nothing -> pure ()
Just s -> print s -- yay, prints the right thing at runtime
Hey, that wasn't so bad! A lot of the intermediate steps are actually deduced by GHC already. But we had to refer to that helper type family with the random number in its name....
Now obviously this is not nice, and IMO is at least a similar problem as the one indicated in the OP. (The OP also talks about unexported helper functions of the Prelude etc functions, which luckily I did not need to write proofs about here. I could file this as a separate issue if you prefer; I don't see another similar one in the issue tracker currently.) I can sort of see your point that the Case_* helper type family is an implementation detail leak that is simply unavoidable, one has to write a proof about it - but surely that random number part of its name is unintended. Even though it seems to be deterministic (yay GHC), it does change if I change the surrounding code even slightly, and I have to update the proof code to match it. I'm also not sure if the number remains stable across different machines or compiler versions, if not then it's not something that can be part of serious code...
I also note that the proof looks suspiciously similar in shape to the implementation (of lookupKV), so wonder if it might be possible to auto-generate it. (GHC already was able to infer basic facts about fmap for example, but I don't see that singletons generates corresponding proofs.) Though I suppose this is getting into research areas now...
Now that looks like an example of what I refer to as "unintended" implementation details. Perhaps "unintended" was not the best choice of phrase in hindsight, since I think if you were to write this proof in another dependently typed language, the details would look pretty similar. The main difference is that in singletons, you have to refer to gensymmed names like Case_6989586621679077040 in order to complete the proof. A proof assistant like Coq, on the other hand, would let you manipulate subexpressions directly without needing to explicitly name them.
If not unintended, then the approach that singletons uses is definitely more fragile. Case in point: I tried to compile your HLookupKVWithProof.hs example from https://github.com/goldfirere/singletons/issues/339#issuecomment-612525798, but it failed due to GHC generating a different unique number for Case:
HLookupKVWithProof.hs:41:16: error:
Not in scope: type constructor or class ‘Case_6989586621679077040’
Perhaps you meant ‘Case_6989586621679077286’ (line 11)
|
41 | class (Fmap f (Case_6989586621679077040 k k' kk v' vv eq) ~
| ^^^^^^^^^^^^^^^^^^^^^^^^
HLookupKVWithProof.hs:42:8: error:
Not in scope: type constructor or class ‘Case_6989586621679077040’
Perhaps you meant ‘Case_6989586621679077286’ (line 11)
|
42 | Case_6989586621679077040 k k' kk (Apply f v') (Fmap f vv) eq)
| ^^^^^^^^^^^^^^^^^^^^^^^^
Unfortunately, this means that this sort of code is inherently nondeterministic.
Alas, I don't see an easy solution to this problem. @goldfirere's suggestion in https://github.com/goldfirere/singletons/issues/339#issuecomment-397156665 will make this less likely to occur, but it likely won't make the issue completely go away. I can't think of a way to completely solve this short of equipping GHC with some way to manipulate subexpressions à la Coq.
Until GHC gains such a power, you can always apply the workaround from (2) in https://github.com/goldfirere/singletons/issues/339#issue-332172197. Namely, factor out the relevant subexpressions to be top-level functions, like so:
singletons [d|
lookupKV :: Eq k => k -> [k] -> [v] -> Maybe v
lookupKV k [] [] = Nothing
lookupKV k (k':kk) (v:vv) = aux k kk v vv (k == k')
aux :: Eq k => k -> [k] -> v -> [v] -> Bool -> Maybe v
aux _ _ v _ True = Just v
aux k kk v vv False = lookupKV k kk vv
|]
...
class (Fmap f (Aux k kk v' vv eq) ~
Aux k kk (Apply f v') (Fmap f vv) eq)
=> Vf f (k :: kt) k' kk v' vv eq where
Well, we can imagine using a little TH magic. The challenge is that the internal functions have nondeterministic names. So we can't hard-code them. But we can reify the top-level expression and then extract the internal name from it. One problem is that TH never preserves value definitions for reification. Could we get to what we want from the promoted version of functions? Probably.
More generally, it seems possible to imagine a tactic-like system that uses TH.
I don't think either of these are good ideas. But they're ideas, nonetheless.