RFC: Singleton equality witnesses

[Gabor Greif]

On 2/5/13, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> I'm glad you've revived the thread, Gabor. My attention has been diverted
> elsewhere, but it's good to move forward with this. Thanks.

Hi Richard,

thanks for the encouragement!

>
> My argument would be not to return
>   Maybe (SameSing kparam a b)
> but to return
>   Either (SameSing kparam a b) (SameSing kparam a b -> Void)
> or something similar. (Void is taken from the void package, but it could

I see where you want to get at and recognize the added value. I have
two thoughts to add, though.

  o most people are comfortable with assembling equality evidence (for
example by means of the Maybe monad), but few have done this for its
refutations.

  o sometimes an equality proof is just what you need to proceed,
which is probably a smaller data structure to be created (laziness may
help here, but still allocates).

So I decided to leave 'sameSing' in and add a new method 'decideSing'
with your semantics. However, I have no idea how to implement the
non-equality pieces of Nat and Symbol. I have punted for now, failing
to add the corresponding branches. Maybe you can come up with
something sensible. Anyway, sameSing now has a default method that
maps positive evidence from decideSing into the Maybe monad.
I also flipped the type arguments to Either, since 'Right' sounds like
"Yep" and should signify positive evidence. I believe the ErrorT monad
transformer also uses this convention. (This is not a political
message, though :-)

> easily be redefined into any empty type.) You're right that empty pattern
> matches are available now (thanks, Simon!) but their usefulness comes into
> play only with the Either type, not with the Maybe type. What you have below
> would certainly be useful, but in my opinion, the Either construction is
> more so.
>
> Also, why generalize the return type with SameSing? Do you have a case where
> you would want the equality witness type to be other than (:~:)?

This leaves open the possibility of non-constructivistic evidence (is
there such a thing?). For example I could imagine an infinite Nat-like
type (with different representation) where we have a refutation proof
that n < m-1 and a refutation of n > m+1, and this would allow us to
construct evidence for n=m. I have seen
http://queuea9.wordpress.com/2012/11/05/canonize-this/ (and more
recent ones).

>
> I've thrown together a wiki page at
> http://hackage.haskell.org/trac/ghc/wiki/TypeLevelReasoning with Gabor's
> code, my code, and some of my thoughts. Please add your thoughts and any
> ideas into the mix!

I have commented on PropNot, suggesting alternatives.


Okay, here is the diff that I have so far:

-------------------------------------------------------------------
index f8b759e..7715a32 100644
--- a/GHC/TypeLits.hs
+++ b/GHC/TypeLits.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE TypeFamilies #-}           -- for declaring operators +
sing family
 {-# LANGUAGE TypeOperators #-}          -- for declaring operator
 {-# LANGUAGE EmptyDataDecls #-}         -- for declaring the kinds
+{-# LANGUAGE EmptyCase #-}              -- for absurd
 {-# LANGUAGE GADTs #-}                  -- for examining type nats
 {-# LANGUAGE PolyKinds #-}              -- for Sing family
 {-# LANGUAGE FlexibleContexts #-}
@@ -30,7 +31,7 @@ module GHC.TypeLits
   , type (-)

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

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

 -- | (Kind) A kind useful for passing kinds as parameters.
 data OfKind (a :: *) = KindParam
@@ -133,6 +136,15 @@ 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)
+  sameSing a b = case decideSing a b of
+                 Right witness -> Just witness
+                 otherwise -> Nothing
+  decideSing :: Sing a -> Sing b -> Decision (SameSing kparam a b)
+
 instance SingE (KindParam :: OfKind Nat) where
   type DemoteRep (KindParam :: OfKind Nat) = Integer
   fromSing (SNat n) = n
@@ -141,6 +153,16 @@ instance SingE (KindParam :: OfKind Symbol) where
   type DemoteRep (KindParam :: OfKind Symbol) = String
   fromSing (SSym s) = s

+instance SingEquality (KindParam :: OfKind Nat) where
+  sameSing = eqSingNat
+  decideSing a b = case eqSingNat a b of
+                   Just witness -> Right witness
+
+instance SingEquality (KindParam :: OfKind Symbol) where
+  sameSing = eqSingSym
+  decideSing a b = case eqSingSym a b of
+                   Just witness -> Right witness
+
 {- | 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 . -}
@@ -236,6 +258,18 @@ data (:~:) :: k -> k -> * where
 instance Show (a :~: b) where
   show Refl = "Refl"

+
+-- | A type that has no inhabitants.
+data Void
+
+-- | Anything follow from falseness.
+absurd :: Void -> a
+absurd x = case x of {}
+
+type Refuted a = a -> Void
+
+type Decision a = Either (Refuted a) a
+
 {- | Check if two type-natural singletons of potentially different types
 are indeed the same, by comparing their runtime representations.
-------------------------------------------------------------------

I haven't exported all parts yet.

What do you think?

Cheers,

    Gabor

>
> Richard
>
> On Feb 5, 2013, at 1:34 PM, Gabor Greif <ggreif at gmail.com> wrote:
>
>> 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
>>>
>>>
>>
>
>