Re: [GHC] #12422: Add decidable equality class

23 Jul 2016

      ...
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