Re: RFC: Singleton equality witnesses

On 2/5/13, Richard Eisenberg 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@. -} @@ -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 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 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@. -} ------------------------------------------------------

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