[Git][ghc/ghc][wip/clarify-test-coercion] Clarify laws of `TestCoercion`

[John Ericson (@Ericson2314)]

John Ericson pushed to branch wip/clarify-test-coercion at Glasgow Haskell Compiler / GHC


Commits:
d343f493 by John Ericson at 2022-12-10T11:44:36-05:00
Clarify laws of `TestCoercion`

- Add law to `TestCoercion` to match `TestEquality`

- Remove recommendation for singleton types because of uncertainty
  whether this is a good recommendation.

- Discuss the singleton type quandary under an [expandable
  heading](https://haskell-haddock.readthedocs.io/en/latest/markup.html?highlight=expandable#headings)
  for anyone that is curious, without cluttering the main documentation.

Follow up from a5ea78673eae7c837a5ccb7882e908a4df92e75d.

- - - - -


1 changed file:

- libraries/base/Data/Type/Coercion.hs


Changes:

=====================================
libraries/base/Data/Type/Coercion.hs
=====================================
@@ -97,9 +97,64 @@ instance Coercible a b => Enum (Coercion a b) where
 -- | @since 4.7.0.0
 deriving instance Coercible a b => Bounded (Coercion a b)
 
--- | This class contains types where you can learn the equality of two types
--- from information contained in /terms/. Typically, only singleton types should
--- inhabit this class.
+-- | This class contains types where you can learn the coercibility of two
+-- types from information contained in /terms/.
+--
+-- The result should be @Just Coercion@ if and only if the types applied to @f@
+-- are coercible:
+--
+-- @testCoercion (x :: f a) (y :: f b) = Just Coercion@ ⟺ Coercible a b@
+--
+-- === __Guidance on use with singleton types__
+--
+-- It was previously recommend that only singleton types should inhabit this
+-- class. However, it is unclear what the singleton types should represent.
+--
+-- Normally, a singleton type has one value per *type*: types quotiented by
+-- nominal equivalence, i.e. just types.
+--
+-- An example of this would be:
+--
+-- @
+--     data Nom0 :: Type -> Type where
+--       Nom0Int  :: Nom0 Int
+--       Nom0Bool :: Nom0 Bool
+-- @
+--
+-- Which, to make relationship to the next part more clear, let's rewrite more
+-- verbosely as:
+--
+-- @
+--     data Nom1 :: Type -> Type where
+--       Nom1Int  :: forall a. a ~ Int  => Nom1 a
+--       Nom1Bool :: forall a. a ~ Bool => Nom1 a
+-- @
+--
+-- But arguably, given that we are testing for coercibility, it would be better
+-- to have one value per *representation*: types quotiented by representational
+-- equivalence, i.e. equivalence classes of types that are
+-- pairwise-'Coercible'.
+--
+-- An example of this would be:
+--
+-- @
+--     data Rep :: Type -> Type where
+--       RepInt  :: forall a. a `Coercible` Int  => Rep a
+--       RepBool :: forall a. a `Coercible` Bool => Rep a
+-- @
+--
+-- The goal of this would be to have laws similar to that for 'TestEquality'
+-- when used with singletons:
+--
+-- @testCoercion (x :: f a) (y :: f b) = Just Refl ⟺ a `Coercible` b ⟺ coerce x = coerce y@
+--
+-- @isJust (testCoercion x y) = coerce x == coerce y@
+--
+-- However, GHC today thinks the argument to 'Rep' must have a nominal role,
+-- and therefore the above doesn't work.
+--
+-- Regardless, singleton types are not required, however, and so the latter
+-- would-be laws are not in fact valid in general.
 class TestCoercion f where
   -- | Conditionally prove the representational equality of @a@ and @b at .
   testCoercion :: f a -> f b -> Maybe (Coercion a b)



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d343f4937706d8f3563b2f07be02710439cacb9d

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d343f4937706d8f3563b2f07be02710439cacb9d
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20221210/92552af1/attachment-0001.html>