RFC: Singleton equality witnesses

[Richard Eisenberg]

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.

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 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 (:~:)?

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!

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