RFC: Singleton equality witnesses

[Gabor Greif]

Richard and all,

sorry for reviving such an ancient thread, but I'd like to move this
forward a bit :-)

In the meantime Iavor has added the (:~:) GADT, so I can reuse it. It
has been commented that it could (finally) end up in GHC.Exts, but for
now I want my changes minimized.

I have added the class @SingEquality@ and have implemented the
@sameSing@ method in terms of Iavor's functions. This is rather pretty
now. Here is the patch:

------------------------------------------------------
$ git show 0eacf265255b9c5e0191b6a5100f3076b8eb5520
commit 0eacf265255b9c5e0191b6a5100f3076b8eb5520
Author: Gabor Greif <ggreif at gmail.com>
Date:   Fri Nov 30 12:23:28 2012 +0100

    Introduce the SingEquality class
    with customizable witness type
    and a sameSing method that may
    produce the latter.

diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs
index f8b759e..5546a5a 100644
--- a/GHC/TypeLits.hs
+++ b/GHC/TypeLits.hs
@@ -30,7 +30,7 @@ module GHC.TypeLits
   , type (-)

     -- * Comparing for equality
-  , type (:~:) (..), eqSingNat, eqSingSym
+  , type (:~:) (..), eqSingNat, eqSingSym, SingEquality (..)

     -- * Destructing type-nat singletons.
   , isZero, IsZero(..)
@@ -56,6 +56,7 @@ import Unsafe.Coerce(unsafeCoerce)
 -- import Data.Bits(testBit,shiftR)
 import Data.Maybe(Maybe(..))
 import Data.List((++))
+import Control.Monad (guard, return, (>>))

 -- | (Kind) A kind useful for passing kinds as parameters.
 data OfKind (a :: *) = KindParam
@@ -133,6 +134,11 @@ class (kparam ~ KindParam) => SingE (kparam ::
OfKind k) where
   type DemoteRep kparam :: *
   fromSing :: Sing (a :: k) -> DemoteRep kparam

+class (kparam ~ KindParam, SingE (kparam :: OfKind k)) =>
SingEquality (kparam :: OfKind k) where
+  type SameSing kparam :: k -> k -> *
+  type SameSing kparam = (:~:)
+  sameSing :: Sing a -> Sing b -> Maybe (SameSing kparam a b)
+
 instance SingE (KindParam :: OfKind Nat) where
   type DemoteRep (KindParam :: OfKind Nat) = Integer
   fromSing (SNat n) = n
@@ -141,6 +147,12 @@ instance SingE (KindParam :: OfKind Symbol) where
   type DemoteRep (KindParam :: OfKind Symbol) = String
   fromSing (SSym s) = s

+instance SingEquality (KindParam :: OfKind Nat) where
+  sameSing = eqSingNat
+
+instance SingEquality (KindParam :: OfKind Symbol) where
+  sameSing = eqSingSym
+
 {- | A convenient name for the type used to representing the values
 for a particular singleton family.  For example, @Demote 2 ~ Integer@,
 and also @Demote 3 ~ Integer@, but @Demote "Hello" ~ String at . -}
------------------------------------------------------

Regarding Richard's decidable equality suggestion, I think this would
be the next step. IIRC, empty case expressions have been implemented,
so GHC HEAD should be prepared.

What do you think? Okay to push in this form?

Cheers,

    Gabor


On 12/5/12, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> I don't think anything here is *high priority*, just musings on how best to
> move forward.
>
> About empty case, consider this:
>
>> data a :~: b where
>>   Refl :: a :~: a
>>
>> absurd :: True :~: False -> a
>
> Now, I want to write a term binding for absurd. GHC can figure out that
> (True :~: False) is an empty type. So, if we have (absurd x = case x of …),
> there are no valid patterns, other than _, that could be used. Instead of
> writing (absurd _ = undefined), I would much prefer to write (absurd x =
> case x of {}). Why? If I compile with -fwarn-incomplete-patterns and
> -Werror, then the latter has no possible source of partiality and yet
> compiles. The former looks dangerous, and GHC doesn't check to make sure
> that, in fact, the function can never get called.
>
> The bottom line, for me at least, is that I want to avoid the partial
> constructs (incomplete patterns, undefined, etc) in Haskell as much as
> possible, especially when I'm leveraging the type system to a high degree.
> The lack of empty case statements forces me to use undefined where it isn't
> really necessary.
>
> I'll leave it to others to comment on TypeRep, as I'm a little hazy there
> myself.
>
> Richard
>
>