SEq vs SDecide, former works better with type checker in certain cases #447
Comments
|
In the case of your particular program, you are directly using boolean equality in the definition of lookupKV k (k':kk) (v:vv) = if k == k' then Just v else lookupKV k kk vvAs a result, you must use boolean equality in order to reduce the This isn't a case of #339, since that issue is about internal implementation details leaking through to the user. On the other hand, the use of boolean equality in module EqVsDecide
%default total
data TMaybe : Maybe k -> Type where
TNothing : TMaybe Nothing
TJust : t -> TMaybe (Just t)
data KVList : List kt -> List Type -> Type where
KVNil : KVList [] []
KVCons : (k : kt) -> v -> KVList kk vv -> KVList (k::kk) (v::vv)
lookupKV : Eq k => k -> List k -> List v -> Maybe v
lookupKV k [] [] = Nothing
lookupKV k (k'::kk) (v::vv) = if k == k' then Just v else lookupKV k kk vv
lookupKV k _ _ = Nothing
hLookupKV : Eq kt => (k : kt) -> KVList kk vv -> TMaybe (lookupKV k kk vv)
hLookupKV k KVNil = TNothing
hLookupKV k (KVCons k' v r) with (k == k')
hLookupKV k (KVCons k' v r) | True = TJust v
hLookupKV k (KVCons k' v r) | False = hLookupKV k r
hLookupKV' : (DecEq kt, Eq kt) => (k : kt) -> KVList kk vv -> TMaybe (lookupKV k kk vv)
hLookupKV' k KVNil = TNothing
hLookupKV' k (KVCons k' v r) with (decEq k k')
hLookupKV' k (KVCons k v r) | Yes Refl = TJust v
hLookupKV' k (KVCons k' v r) | No _ = hLookupKV' k rNotice that Idris is unable to reduce |
|
OK, thanks I can appreciate that they are distinct concepts and can't be mixed. I'm guessing that "boolean equality" means "related to the Eq class and its promoted variants" and "propositional equality" means "from the viewpoint of the GHC / Haskell type checker attempting unification", hopefully this is an accurate of putting it? So in theory if singletons, when promoting Does that feature even make sense? As I understand, it's not possible in Haskell to declare that two term-level variables are equal, but on the type-level we can do this, so singletons could theoretically translate this to propositional instead of boolean equality. (I'm not asking for the feature, I don't have an immediate use for it; I'm just trying to confirm my understanding by predicting something.) Then (I did not try doing this manually yet, as I don't know what the promoted analogue of If my understanding based on your explanation is correct, then having |
Boolean equality is a simple form of equality that checks if two things are equal and returns a simple "yes" or "no" answer (i.e., a
Short answer: there is no easy way to promote Long answer: To see if what you describe is possible, let's go back to the Idris version of the program. We can define a variant of lookupKV : DecEq k => k -> List k -> List v -> Maybe v
lookupKV k [] [] = Nothing
lookupKV k (k'::kk) (v::vv) with (decEq k k')
lookupKV k (k ::kk) (v::vv) | Yes Refl = Just v
lookupKV k (k'::kk) (v::vv) | No _ = lookupKV k kk vv
lookupKV k _ _ = NothingHaving done this, if we then define hLookupKV' : DecEq kt => (k : kt) -> KVList kk vv -> TMaybe (lookupKV k kk vv)
hLookupKV' k KVNil = TNothing
hLookupKV' k (KVCons k' v r) with (decEq k k')
hLookupKV' k (KVCons k v r) | Yes Refl = TJust v
hLookupKV' k (KVCons k' v r) | No _ = hLookupKV' k rThen it typechecks! This good news, since making this program work a language with native support for dependent types hints at the possibility that we could encode it with $(singletons [d|
lookupKV :: Decide k => k -> [k] -> [v] -> Maybe v
lookupKV k [] [] = Nothing
lookupKV k (k':kk) (v:vv) =
case k %~ k' of
Proved Refl -> Just v
Disproved _ -> lookupKV k kk vv
|])There are numerous problems with this idea, but the most notable problem is that we can't define a "simply typed" version of That being said, we might be able to accomplish this if we are willing to get our hands dirty. First, we need to define a class PDecide k where
type (a :: k) :~ (b :: k) :: PDecision (a :~: b)(I'll define While GHC doesn't have full-spectrum dependent types, it does have visible dependent quantification at the kind level. Note that the full kind of The next step is to change class SDecide k where
(%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :~ b)In order to make that work, we'll need a singled version of data (%:~:) :: forall a b. a :~: b -> Type where
SRefl :: (%:~:) Refl
type instance Sing = (%:~:)
data Decision' p a
= Proved a
| Disproved (p @@ a @@ Void)
type Decision = Decision' (TyCon2 (->))
type PDecision = Decision' (~>@#@$)
data SDecision :: forall a. PDecision a -> Type where
SProved :: forall a (x :: a). Sing x -> SDecision (Proved x)
SDisproved :: forall a (r :: a ~> Void). Sing r -> SDecision (Disproved r)
type instance Sing = SDecision(Note that I'm using a trick from #82 to allow With this out of the way, we can now define a version of type family LookupKV (a :: k) (as :: [k]) (bs :: [v]) :: Maybe v where
LookupKV k '[] '[] = Nothing
LookupKV k (k':kk) (v:vv) = Case k k' (k :~ k') kk v vv
type family Case (a :: k) (a' :: k) (pd :: PDecision ((a :: k) :~: a')) (as :: [k])
(b :: v) (bs :: [v]) :: Maybe v where
Case k k (Proved Refl) kk v vv = Just v
Case k k' (Disproved _) kk v vv = LookupKV k kk vvAnd finally, a version of hLookupKV'
:: SDecide 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
SProved SRefl -> TJust v
SDisproved _ -> hLookupKV' sk remPhew, that was a lot of work! But this does demonstrate that all of this is technically possible. The tricky part, then, is figuring out how you might get Template Haskell to generate all of this code:
My belief is that we're a long ways away from accomplishing this. For these reasons, I think it's best to stick to the simpler version of |
|
Thank you very much for that detailed explanation and expansion! That confirms what I thought I understood from your previous comments. I can certainly understand that doing this automatically in TH is a long way off, and am in no hurry to want this potential feature.
|
|
It's not unheard of to implement certain definitions in |
|
I may have just found a use case for it. Suppose we want to do something based on a runtime value, we can use {-# LANGUAGE DataKinds, GADTs, KindSignatures, ScopedTypeVariables, TypeApplications #-}
import Data.Text (pack)
import Data.Singletons.Decide
import Data.Singletons.Prelude
import Data.Singletons.TypeLits
main = do
let k0 = SSym @"a"
withSomeSing (pack "a") $ \(k :: Sing (kt :: Symbol)) -> do
{-case k0 %== k of
STrue -> print "yes" -- error: ‘a0’ is untouchable inside the constraints: DefaultEq "a" a ~ 'True
SFalse -> print "no" -- similar error -}
case k0 %~ k of
Proved Refl -> print "yes"
Disproved _ -> print "no"This also affects the other code I've been writing - the proof-constraints cannot be satisfied inside a Or is there another way of doing this with |
|
That's just due to a limitation of GHC's type inference, I believe. It will typecheck if you add a type signature to main :: IO ()
main = do
let k0 = SSym @"a"
withSomeSing (pack "a") $ \(k :: Sing (kt :: Symbol)) -> do
case k0 %== k of
STrue -> print "yes"
SFalse -> print "no" |
|
Ah, it turns out I had a signature, but I was testing my example by commenting out only the main :: IO ()
main = do
let k0 = SSym @"a" :: Sing ("a" :: Symbol)
--let k = SSym @"b"
withSomeSing (pack "a") $ \(k :: Sing (kt :: Symbol)) -> do
(case k0 %== k of
STrue -> print "yes"
SFalse -> print "no") :: IO () -- explicit type signature needed...
case k0 %~ k of
Proved Refl -> print "yes"
Disproved _ -> print "no"That was a red herring; the real problem I was having, is that if your proofs rely on class Wf k kk where
instance Wf k '[]
instance (Vf (k == k1)) => Wf k (k1 ': kk)
class Vf eq where
instance Vf 'True
instance Vf 'False
vf :: Vf (k == k1) => Sing k -> Sing k1 -> IO ()
vf k k' = pure ()
wf :: Wf k kk => Sing k -> Sing kk -> IO ()
wf k k' = pure ()
main :: IO ()
main = do
let k0 = SSym @"a" :: Sing ("a" :: Symbol)
let kk = sing :: Sing ('["a" :: Symbol])
vf k0 k0 >> wf k0 kk
withSomeSing (pack "a") $ \(k :: Sing (kt :: Symbol)) -> do
-- vf k0 k -- No instance for (Vf (DefaultEq "a" a)) arising from a use of ‘vf’
-- vf k k0 -- No instance for (Vf (DefaultEq a "a")) arising from a use of ‘vf’
-- wf k kk -- No instance for (Vf (DefaultEq a "a")) arising from a use of ‘wf’
-- potential workarounds below:
(_ :: ()) <- case k %== k0 of
STrue -> vf k k0 >> wf k kk
SFalse -> vf k k0 >> wf k kk
(_ :: ()) <- case k0 %== k of -- note, only difference is order of comparison
STrue -> vf k0 k -- vf k k0 >> wf k kk -- Could not deduce (Vf (DefaultEq a "a"))
SFalse -> vf k0 k -- vf k k0 >> wf k kk -- Could not deduce (Vf (DefaultEq a "a"))
case k0 %~ k of
Proved Refl -> vf k0 k >> vf k k0 >> wf k kk
Disproved _ -> pure () -- vf k0 k >> vf k k0 >> wf k kk -- No instance for (Vf (DefaultEq "a" a))
case k %~ k0 of
Proved Refl -> vf k0 k >> vf k k0 >> wf k kk
Disproved _ -> pure () -- vf k0 k >> vf k k0 >> wf k kk -- No instance for (Vf (DefaultEq "a" a))Perhaps you can understand the behaviour a bit better; my current guess at understanding it is that, one can recover enough types for GHC to deduce the constraints, by applying runtime functions involving This would seem to put a dampener on the whole technique of encoding proofs as constraints - if you want resolution based on runtime types that is; so I suppose the fix will have to involve encoding proofs using the runtime Separately and before I realised the above, I attempted to fix it by building on top of your instance PDecide Symbol where
type a :~ a = 'Proved 'Refl
-- Expected kind ‘((~>@#@$) @@ (a :~: b)) @@ Void’
-- we want to find constructors with type ((a :~: b) ~> Void) then promote it to the kind level
-- but TyFun / (~>) do not have constructors
type a :~ b = 'Disproved {-- what goes here? --}Not sure if this is just because of the fact that your code was a toy example, or because of my missing knowledge about the library. Anyway after the above reasoning, I believe even if this worked, it wouldn't actually fix my problem since it's unrelated to how the constraints are being resolved. By the way, thank you for being patient with all of my questions which might seem a bit basic. I hope this discussion will be useful for other people - I am trying to do some stuff that is a bit more complex than the typical basic tutorials on dependent types, but that is fairly reasonable and intuitively-desired for "real world" use cases I think, so hopefully this brings us all some experience on how to communicate about these languages & techniques better to more people. |
|
At the risk of sounding like a broken record, the type errors you're experiencing are just a symptom of GHC's inability to perform type inference underneath GADT pattern matches. In particular, GHC is reluctant to infer types underneath equality constraints. Here is a very small example from Section 5.1 of the paper OutsideIn(X), which is the standard reference for how GADT type inference works: {-# LANGUAGE GADTs #-}
module Foo where
data T a where
T1 :: Int -> T Bool
f = \x -> case x of { T1 n -> n > 0 }Like several of your prior examples, this will fail to typecheck: The difficulty here is that This is not to say that GHC cannot perform any type inference under GADT pattern matches. Section 5.1 of OutsideIn(X) also makes a note of this example which GHC is able to infer a type for: {-# LANGUAGE GADTs #-}
module Foo where
data T a where
T1 :: Int -> T Bool
T2 :: T a
-- g :: T a -> Bool
g = \x -> case x of { T1 n -> n > 0; T2 -> True }This time, Personally speaking, I find this constraint solving process difficult to predict, so I almost always err on the side of giving explicit type signatures. Sometimes, this means breaking things up into smaller pieces: main :: IO ()
main = do
let k0 = SSym @"a"
withSomeSing (pack "a") $ \(k :: Sing (kt :: Symbol)) -> do
let step1 :: IO ()
step1 =
case k0 %== k of
STrue -> print "yes"
SFalse -> print "no"
step2 :: IO ()
step2 =
case k0 %~ k of
Proved Refl -> print "yes"
Disproved _ -> print "no"
step1
step2
I'm not quite sure what you mean by "passing theorems around".
We can take inspiration from the current singletons/src/Data/Singletons/TypeLits/Internal.hs Lines 97 to 103 in 779b8cc
$(singletons [d|
disprovedSymbol :: a :~: b -> Void
disprovedSymbol _ = error "Broken Symbol singletons"
|])
type family DecideSymbol (a :: Symbol) (b :: Symbol) :: PDecision (a :~: b) where
DecideSymbol a a = Proved Refl
DecideSymbol a b = Disproved DisprovedSymbolSym0
instance PDecide Symbol where
type a :~ b = DecideSymbol a b
instance SDecide Symbol where
(SSym :: Sing n) %~ (SSym :: Sing m)
| Just Refl <- GHC.TypeLits.sameSymbol (Proxy :: Proxy n) (Proxy :: Proxy m)
= SProved SRefl
| otherwise
= unsafeCoerce $ SDisproved (singFun1 @DisprovedSymbolSym0 sDisprovedSymbol) |
|
Sorry, I don't think my problem was the lack of type signatures, I really did add plenty already. But I think I've figured out the problem in the meanwhile, here is the solution: In the example over in #339 I encoded a proof as a constraint, of How this proof works is by induction, but when GHC actually comes to selecting an instance, it steps through the proof with the type variables instantiated to real types. Intuitively speaking, it "runs" the proof for a single case, it doesn't prove the proof for all cases. This doesn't work if the type is a runtime type like To make this work, one has to do a case-match underneath a This was where I got stuck yesterday, but I realised that you can write a recursive Continuing from the example over in #339: -- | Prove @Wf f k kk vv@. You need this inside a @withSomeSing@ and other
-- similar constraints involving a runtime 'k', in order to bring the
-- @Wf f k kk vv@ constraint into scope, to use certain utility functions like
-- 'withLookupKV' that require this constraint, representing a theorem.
withSomeWf
:: forall f (k :: kt) (kk :: [kt]) vv r
. SEq kt
=> Proxy f
-> Sing k
-> KVList kk vv
-> (Wf f k kk vv => r)
-> r
withSomeWf _ k KVNil c = c
withSomeWf p k (KVCons k' v tab) c = case k %== k' of
STrue -> withSomeWf p k tab c
SFalse -> withSomeWf p k tab c
main :: IO ()
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
let k0 = SSym @"a"
let k1 = SSym @"b"
void $ traverse print $ withLookupKV v k0 c
withSomeSing (pack "a") $ \k -> do
-- without this line, GHC fails with:
-- No instance for (Vf (FlipSym2 (TyCon2 (->)) [Char]) {..etc..} (DefaultEq a "a"))
-- arising from a use of ‘withLookupKV’
withSomeWf (Proxy @(FlipSym2 (TyCon2 (->)) [Char])) k v $ do
void $ traverse print $ withLookupKV v k c(And yes, later I'll probably switch on
I thought that a solution might require passing some term around that represents the proof, and then each function would case-match on this term to bring the proof into scope. The solution above uses the "with-continuation" pattern instead, which is nicer since it only has to be used once, and no term-level proofs are needed. This alternative technique might have some advantages such as avoiding the constraint solver and its slightly opaque error messages, although I did not try it yet because it's not clear to me how to encode I think this covers all of my use-cases, so hopefully I won't have any more questions! Thanks for all your help so far. I will try to write all of this up at some point as a guide for anyone else trying to do similar things. |
My apologies. There have been a multitude of examples discussed in this issue, so I likely had a different example in mind than the one you were referring to. (The examples in #447 (comment) definitely suffered from a lack of type signatures.)
I don't think I'm experienced enough in either Agda or Idris to say with certainty whether encoding proofs as implicit arguments is "conventional" or not. I do know that type class resolution works differently in Haskell than in languages like Agda/Idris, since the former enforces global coherence of class instances, while the latter do not. That doesn't necessarily mean that it's impossible to write implicit-arguments-as-proofs–style code in these languages, but the ergonomics might be different.
I suppose it depends on your perspective. If you look at the implementation of
Wonderful! Does this mean that this issue can be closed? |
|
Sounds good, there is nothing actionable on the singletons library here. Perhaps later I will come up with some documentation suggestions. |
(Continued from https://gitlab.haskell.org/ghc/ghc/issues/18035)
Consider the following code, an attempt to implement a heterogeneous association list:
{-# LANGUAGE ConstraintKinds, DataKinds, GADTs, PolyKinds, ScopedTypeVariables, TemplateHaskell, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-} import Data.Kind import Data.Singletons.Decide import Data.Singletons.Prelude import Data.Singletons.TH import Unsafe.Coerce (unsafeCoerce) -- heterogeneous Maybe that carries the type data TMaybe (t :: Maybe k) where TNothing :: TMaybe 'Nothing TJust :: !t -> TMaybe ('Just t) -- heterogeneous assoc list -- kk is separate from vv for easier unification data KVList (kk :: [kt]) (vv :: [Type]) :: Type where KVNil :: KVList '[] '[] KVCons :: !(Sing (k :: kt)) -> !(v :: Type) -> !(KVList kk vv) -> KVList (k : kk) (v : vv) 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 |] 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 -- This version doesn't type-check! -- It's similar to the one in the original post, except -- it uses singleton's autogenerated LookupKV type family -- instead of the manually-written one. hLookupKV' :: SDecide 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 Proved Refl -> TJust v Disproved _ -> unsafeCoerce (hLookupKV' (unsafeCoerce sk) (unsafeCoerce rem)) -- ^ even unsafeCoerce doesn't help, we are still left with "could not deduce" errorsAs you can see, the difference between the working and non-working versions are solely down to the choice of
SEqvsSDecide. I'm unsure if this is a case of #339, but if it's expected behaviour then perhaps it should be added to the documentation.SEqwould seem to fit better into the rest of the singletons framework, and it's unclear what the differences between it andSDecideare, or how their intended use cases differ.Another thing that is confusing / blocking my understanding, is that the implementation for
DefaultEqseems to do the very thing I did at the top of GHC #18035 where we have an overlapping type family declaration, yet somehow it works for singletons. The unsafeCoerce workaround that was cited is only forSEq TypewhereasDefaultEqis used for most other types/kinds, it would seem.The text was updated successfully, but these errors were encountered: