Implementation details are needed for proofs #339
Comments
|
What you want is reasonable. And perhaps key functions, like 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 |
|
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
|
|
Yes, that's just what I was thinking, if you wanted to implement it. :) |
|
It looks like this problem will strike in more places in the upcoming {-# 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
-> ReflBut not with The culprit is that I changed the definition of singletons/src/Data/Singletons/Prelude/List.hs Lines 359 to 361 in 8aeba2a To this (in singletons/src/Data/Singletons/Prelude/Foldable.hs Lines 600 to 602 in 60dd52c Just like the issue with |
|
For any readers out there who are interested in fixing this bug, I've just pushed a Edit: The |
|
Another example, related to -- 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 -- 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 |
|
Note: I wrote that last example 3 before I posted #447 so it still uses |
|
Another set of examples, this one relating to constraints instead of 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 -- 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 tabNow 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 SomeCxtValSo, another phyrric victory, since we had to duplicate a utility function 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 #447 (comment), 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
Trying it by hand, we could do something like this: 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 runtimeHey, 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 I also note that the proof looks suspiciously similar in shape to the implementation (of |
|
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 If not unintended, then the approach that 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 #339 (comment) 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 #339 (comment). 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. |
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 uselet/wherecreate 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.
Both cases fail with a similar error
The issue is that the
goinfoldr, when promoted, gets an (unused) argument that representsfoldr'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 writesumIs.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: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.).The text was updated successfully, but these errors were encountered: