[GHC] #12422: Add decidable equality class
#12422: Add decidable equality class -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Core | Version: 8.0.1 Libraries | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Currently, we have a `TestEquality` class {{{#!hs class TestEquality f where testEquality :: f a -> f b -> Maybe (a :~: b) }}} It would be nice to add a class for fully decidable equality. There are a few options, but this one gets to the point rather quickly: {{{#!hs data EqDec a b where NotEqual :: (forall c . a :~: b -> c) -> EqDec a b Equal :: EqDec a a class DecEq f where decEq :: f a -> f b -> EqDec a b }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12422 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12422: Add decidable equality class -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Shouldn't this go via the libraries list? While what you have there works, I might prefer {{{#!hs type Refuted = a -> Void data Decision a = Yes a | No (Refuted a) class DecideEquality f where -- name lines up with TestEquality decideEquality :: f a -> f b -> Decision (a :~: b) }}} This solution does have one more level of indirection, but it allows you to extract an `a :~: b` from the `Decision`, which will compose better with the other functions from `Data.Type.Equality`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12422#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12422: Add decidable equality class -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Quick thought, is it possible to create a heterogeneous version of `TestEquality` that supports {{{#!hs eqTyCon :: forall (k1 k2 :: *). forall (a :: k1) (b :: k2). TTyCon <k1> a -> TTyCon <k2> b -> Maybe (a :~~: b) }}} Replacing `Maybe (a :~: b)` with `Maybe (a :~~: b)` would still constraint the kinds, would we need {{{#!hs class HTestEquality f1 f2 where htestEquality :: f1 a -> f2 b -> Maybe (a :~~: b) }}} ---- Discussed on `#ghc`, what would break if we made `:~:` heterogeneous? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12422#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12422: Add decidable equality class -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): There are several fun things to respond to here! 1. Making `:~:` heterogeneous would likely break client code. The problem is that, right now, if I say `(Int :~: a)` somewhere, GHC can know that `a :: Type`. If we make `:~:` hetero, then GHC would rightly have `a :: k`, which can cause trouble. This is not hypothetical: I tried making this change once upon a time, and things broke. Even worse, it was hard to go from the error message reported to the actual cause. I advocate against this change. 2. We should have `:~~:` in the standard library. But I was too exhausted from implementing `TypeInType` to start this debate on the libraries mailing list. We should really put it in for 8.2. 3. Here is the hetero version of `TestEquality`: {{{ -- hetero class HTestEquality (f :: forall k. k -> Type) where hTestEquality :: f a -> f b -> Maybe (a :~~: b) }}} Note that `f` has to be polymorphic in its kind to avoid constraining `a` and `b` to have the same kind. Yes, this is a higher-rank kind! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12422#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12422: Add decidable equality class -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Replying to [comment:3 goldfire]:
Yes, this is a higher-rank kind! Yikes! :)
1. Making `:~:` heterogeneous would likely break client code.
2. We should have `:~~:` in the standard library. But I was too exhausted from implementing `TypeInType` to start this debate on the
Figured as much. Is there any way to combine visible kind application (#12045) and unifying different type applications (#11385), let's say if I want to write something like {{{#!hs -- (:~~:) :: forall k1 k2. k1 -> k2 -> Type type (:~:) = (:~~:) @k @k :: k -> k -> Type -- using your syntax (visible kind abstraction?) type (:~:) = \@k -> (:~~:) @k @k }}} libraries mailing list. We should really put it in for 8.2. Should I add it to `Data.Type.Equality` on Phab? ---- Should we rewrite `Const :: Type -> k -> Type` to have the kind ...? {{{#!hs data Const :: Type -> forall k. k -> Type where Const :: { getConst :: a } -> Const a b }}} Is there any way to define an `HTestEquality (Const e)` instance? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12422#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12422: Add decidable equality class -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:4 Iceland_jack]:
Figured as much. Is there any way to combine visible kind application (#12045) and unifying different type applications (#11385), let's say if I want to write something like
{{{#!hs -- (:~~:) :: forall k1 k2. k1 -> k2 -> Type
type (:~:) = (:~~:) @k @k :: k -> k -> Type
-- using your syntax (visible kind abstraction?) type (:~:) = \@k -> (:~~:) @k @k }}}
This is an interesting thought. It can be done in today's syntax: {{{#!hs type (:~:) = ((:~~:) :: k -> k -> Type) pattern Refl :: () => (a ~ b) => a :~: b pattern Refl = HRefl }}} I wonder what the consequences are (if any) of reimplementing `:~:` and `Refl` this way.
2. We should have `:~~:` in the standard library. But I was too
exhausted from implementing `TypeInType` to start this debate on the libraries mailing list. We should really put it in for 8.2.
Should I add it to `Data.Type.Equality` on Phab?
This should be a proposal to the libraries mailing list first. What supporting functions will you have? Perhaps if we use the pattern synonym approach for `:~:` then many existing functions can be reused. I'd be quite pleased if you spearhead this!
----
Should we rewrite `Const :: Type -> k -> Type` to have the kind ...?
{{{#!hs data Const :: Type -> forall k. k -> Type where Const :: { getConst :: a } -> Const a b }}}
Yes. This is slightly more general than quantifying over `k` at the top.
Is there any way to define an `HTestEquality (Const e)` instance?
No. Why would you think there is? `HTestEquality (Const e)` (with your new `Const`) is well-kinded, but I can't imagine an implementation for `hTestEquality`. In general, it's best to quantify over kinds as late as possible, because GHC can't reshuffle where the quantifications are like it can in terms. (When we get `-XDependentTypes`, this deficiency will be resolved.) It may not be worth the effort, but in theory, we should redefine datatypes to have kind quantifications as far to the right as possible. This includes the following preferred declaration for `:~~:`: {{{ data (:~~:) :: forall k1. k1 -> forall k2. k2 -> Type where HRefl :: a :~~: a }}} Sadly, then, there seems to be no way to define `:~:` in terms of `:~~:`. GHC just isn't smart enough to get the kind quantification to work. (Relatedly: kind quantification around type synonyms is very murky and not quite specified.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12422#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12422: Add decidable equality class -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Replying to [comment:5 goldfire]:
This should be a proposal to the libraries mailing list first. What supporting functions will you have? Perhaps if we use the pattern synonym approach for `:~:` then many existing functions can be reused. I'd be quite pleased if you spearhead this!
I wonder what the consequences are (if any) of reimplementing `:~:` and `Refl` this way.
I've tried it with every occurrence of `:~:` in base and it seems to work fine, quite a few functions became more general as a result. The change means `show Refl == show HRefl` (unless we use some type class magic) and {{{#!hs instance a ~~ b => Read ((a::k1) :~~: (b::k2)) where readsPrec d = readParen (d > 10) (\r -> [(HRefl, s) | ("HRefl",s) <- lex r ]) instance a ~~ b => Enum ((a::k1) :~~: (b::k2)) instance a ~~ b => Bounded ((a::k1) :~~: (b::k2)) }}} One downside: You may intend to use heterogeneous equality with `HRefl` but something else unifies the kinds without your knowledge. ---- Does it make sense for `Coercible` / `Coercion` to be heterogeneous? {{{#!hs repr :: forall k1 k2 (a::k1) (b::k2). a :~~: b -> Coercion a b }}} ---- Some weirdness about ordering of kind variables: {{{#!hs data (a::k1) :~~: (b::k2) where HRefl :: a :~~: a -- instance forall k2 k1 (a :: k1) (b :: k2). Show (a :~~: b) deriving instance Show (a :~~: b) }}} `k2` appears before `k1`, I can't remember if this was fixed but this gives you the right order `Show ((a::k1) :~~: (b::k2))`. ---- Given {{{#!hs import GHC.Types data (a::k1) :~~: (b::k2) where HRefl :: a :~~: a pattern Refl :: () => (a ~ b) => (a::k) :~: (b::k) pattern Refl = HRefl type (:~:) = ((:~~:) :: k -> k -> Type) }}} Why does this work?? Shouldn't `Refl` constrain the kinds? {{{#!hs -- instance forall k1 k2 (a :: k1) (b :: k2). (a :: k1) ~~ (b :: k2) => Bounded (a :~~: b) instance a ~~ b => Bounded ((a::k1) :~~: (b::k2)) where minBound = Refl maxBound = Refl }}} ----
No. Why would you think there is?
Actually with the [https://github.com/koengit/KeyMonad/blob/master/paper.lhs Key monad] I was able to write an implementation. I'll post it in a follow up reply.
Sadly, then, there seems to be no way to define `:~:` in terms of `:~~:`. GHC just isn't smart enough to get the kind quantification to work. (Relatedly: kind quantification around type synonyms is very murky and not quite specified.)
I assume `:~:` in terms of `(:~~:) :: forall k1. k1 -> forall k2. k2 -> Type`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12422#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
The `base` library `Data.Typeable` provides similar functionality to the Key monad. Typeable is a type class that provides a value-level representation of the types that implement it. The `Typeable` library
#12422: Add decidable equality class -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): This is what I missed from the paper: provides a function
{{{#!hs eqT :: forall a b. (Typeable a, Typeable b) => Maybe (a :~: b) }}}
where `(:~:)` is the GADT from Figure .... This function gives `Just
Refl` if both ''types'' are the same, whereas `testEquality` from the Key monad only gives `Just Refl` if the ''keys'' are the same. If we have two keys with the same type, but which originate from different `newKey` invocations, the result of `testEquality` will be `Nothing`. My initial thought was ‘if we only had `Typeable` constraints’: {{{#!hs class HTestEquality (f :: forall k. k -> Type) where hTestEquality :: (Typeable a, Typeable b) => f a -> f b -> Maybe (a :~~: b) instance HTestEquality (Const' e) where hTestEquality :: forall a b. (Typeable a, Typeable b) => Const' e a -> Const' e b -> Maybe (a :~~: b) hTestEquality Const'{} Const'{} = heqT @a @b heqT :: forall a b. (Typeable a, Typeable b) => Maybe (a :~~: b) heqT = do guard (typeRep (Proxy :: Proxy a) == typeRep (Proxy :: Proxy b)) pure (unsafeCoerce HRefl) }}} But then I remembered this line from the Key monad paper:
This gives us a form of dynamic typing, ''without'' the need for `Typeable` constraints.
[https://github.com/koengit/KeyMonad/blob/master/KeyM.hs KeyM] with some modifications {{{#!hs -- data Key s a = Key Name data Key :: forall k1. k1 -> forall k2. k2 -> Type where Key :: Name -> Key s a }}} and define {{{#!hs class HTestEquality (f :: forall k. k -> Type) where hTestEquality :: f a -> f b -> Maybe (a :~~: b) instance HTestEquality (Key s) where hTestEquality :: Key s a -> Key s b -> Maybe (a :~~: b) hTestEquality (Key i) (Key j) = do guard (i == j) pure (unsafeCoerce HRefl) instance HTestEquality (Const' e) where hTestEquality :: forall a b. Const' e a -> Const' e b -> Maybe (a :~~: b) hTestEquality Const'{} Const'{} = runKeyM $ do a_key <- newKey @a b_key <- newKey @b pure (a_key =?= b_key) }}} But `a_key` and `b_key` come from different `newKey` invocations, so they will always equal `Nothing`... oh well. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12422#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12422: Add decidable equality class -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12422#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12422: Add decidable equality class -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by int-index): * cc: int-index (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12422#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC