Name changes and addition of gcastWith and (==) to Data.Type.Equality.
authorRichard Eisenberg <eir@cis.upenn.edu>
Mon, 21 Oct 2013 03:43:16 +0000 (23:43 -0400)
committerRichard Eisenberg <eir@seas.upenn.edu>
Mon, 28 Oct 2013 17:15:20 +0000 (13:15 -0400)
For more info, see
http://ghc.haskell.org/trac/ghc/wiki/TypeLevelNamingIssues

Data/Either.hs
Data/Type/Equality.hs
GHC/TypeLits.hs

index b494e26..c0574d5 100644 (file)
@@ -1,6 +1,7 @@
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE DeriveDataTypeable, StandaloneDeriving #-}
+{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -31,6 +32,7 @@ import GHC.Show
 import GHC.Read
 
 import Data.Typeable
+import Data.Type.Equality
 
 {-
 -- just for testing
@@ -103,6 +105,13 @@ isRight :: Either a b -> Bool
 isRight (Left  _) = False
 isRight (Right _) = True
 
+-- instance for the == Boolean type-level equality operator
+type family EqEither a b where
+  EqEither (Left x)  (Left y)  = x == y
+  EqEither (Right x) (Right y) = x == y
+  EqEither a         b         = False
+type instance a == b = EqEither a b
+
 {-
 {--------------------------------------------------------------------
   Testing
index dd0ff3f..e55e473 100644 (file)
@@ -1,10 +1,15 @@
-{-# LANGUAGE DeriveGeneric      #-}
-{-# LANGUAGE TypeOperators      #-}
-{-# LANGUAGE GADTs              #-}
-{-# LANGUAGE FlexibleInstances  #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE NoImplicitPrelude  #-}
-{-# LANGUAGE PolyKinds          #-}
+{-# LANGUAGE DeriveGeneric        #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE GADTs                #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE StandaloneDeriving   #-}
+{-# LANGUAGE NoImplicitPrelude    #-}
+{-# LANGUAGE PolyKinds            #-}
+{-# LANGUAGE RankNTypes           #-}
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ExplicitNamespaces   #-}
 
 -----------------------------------------------------------------------------
 -- |
 
 
 
-module Data.Type.Equality where
+module Data.Type.Equality (
+  -- * The equality type
+  (:~:)(..),
+  
+  -- * Working with equality
+  sym, trans, castWith, gcastWith, apply, inner, outer,
+
+  -- * Inferring equality from other types
+  EqualityType(..),
+
+  -- * Boolean type-level equality
+  type (==)
+  ) where
 
 import Data.Maybe
 import GHC.Enum
@@ -55,8 +72,12 @@ trans :: (a :~: b) -> (b :~: c) -> (a :~: c)
 trans Refl Refl = Refl
 
 -- | Type-safe cast, using propositional equality
-subst :: (a :~: b) -> a -> b
-subst Refl x = x
+castWith :: (a :~: b) -> a -> b
+castWith Refl x = x
+
+-- | Generalized form of type-safe cast using propositional equality
+gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r
+gcastWith Refl x = x
 
 -- | Lift equality into a unary type constructor
 liftEq :: (a :~: b) -> (f a :~: f b)
@@ -99,10 +120,125 @@ instance a ~ b => Bounded (a :~: b) where
 -- | 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.
-class EqualityT f where
+class EqualityType f where
   -- | Conditionally prove the equality of @a@ and @b@.
-  equalsT :: f a -> f b -> Maybe (a :~: b)
-
-instance EqualityT ((:~:) a) where
-  equalsT Refl Refl = Just Refl
+  maybeEquality :: f a -> f b -> Maybe (a :~: b)
 
+instance EqualityType ((:~:) a) where
+  maybeEquality Refl Refl = Just Refl
+
+-- | A type family to compute Boolean equality. Instances are provided
+-- only for /open/ kinds, such as @*@ and function kinds. Instances are
+-- also provided for datatypes exported from base. A poly-kinded instance
+-- is /not/ provided, as a recursive definition for algebraic kinds is
+-- generally more useful.
+type family (a :: k) == (b :: k) :: Bool
+infix 4 ==
+
+-- all of the following closed type families are local to this module
+type family EqStar (a :: *) (b :: *) where
+  EqStar a a = True
+  EqStar a b = False
+
+-- This looks dangerous, but it isn't. This allows == to be defined
+-- over arbitrary type constructors.
+type family EqArrow (a :: k1 -> k2) (b :: k1 -> k2) where
+  EqArrow a a = True
+  EqArrow a b = False
+
+type family EqBool a b where
+  EqBool True  True  = True
+  EqBool False False = True
+  EqBool a     b     = False
+
+type family EqOrdering a b where
+  EqOrdering LT LT = True
+  EqOrdering EQ EQ = True
+  EqOrdering GT GT = True
+  EqOrdering a  b  = False
+
+type EqUnit (a :: ()) (b :: ()) = True
+
+-- more complicated types need a type-level And:
+type family a && b where
+  False && x = False
+  True  && x = x
+  x && False = False
+  x && True  = x
+  x && x     = x
+infixr 3 &&
+
+type family EqList a b where
+  EqList '[]        '[]        = True
+  EqList (h1 ': t1) (h2 ': t2) = (h1 == h2) && (t1 == t2)
+  EqList a          b          = False
+
+type family EqMaybe a b where
+  EqMaybe Nothing  Nothing  = True
+  EqMaybe (Just x) (Just y) = x == y
+  EqMaybe a        b        = False
+
+type family Eq2 a b where
+  Eq2 '(a1, b1) '(a2, b2) = a1 == a2 && b1 == b2
+
+type family Eq3 a b where
+  Eq3 '(a1, b1, c1) '(a2, b2, c2) = a1 == a2 && b1 == b2 && c1 == c2
+
+type family Eq4 a b where
+  Eq4 '(a1, b1, c1, d1) '(a2, b2, c2, d2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2
+
+type family Eq5 a b where
+  Eq5 '(a1, b1, c1, d1, e1) '(a2, b2, c2, d2, e2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2
+
+type family Eq6 a b where
+  Eq6 '(a1, b1, c1, d1, e1, f1) '(a2, b2, c2, d2, e2, f2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2
+
+type family Eq7 a b where
+  Eq7 '(a1, b1, c1, d1, e1, f1, g1) '(a2, b2, c2, d2, e2, f2, g2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2
+
+type family Eq8 a b where
+  Eq8 '(a1, b1, c1, d1, e1, f1, g1, h1) '(a2, b2, c2, d2, e2, f2, g2, h2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2
+
+type family Eq9 a b where
+  Eq9 '(a1, b1, c1, d1, e1, f1, g1, h1, i1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2
+
+type family Eq10 a b where
+  Eq10 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2
+
+type family Eq11 a b where
+  Eq11 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2
+
+type family Eq12 a b where
+  Eq12 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2 && l1 == l2
+
+type family Eq13 a b where
+  Eq13 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2 && l1 == l2 && m1 == m2
+
+type family Eq14 a b where
+  Eq14 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2 && l1 == l2 && m1 == m2 && n1 == n2
+
+type family Eq15 a b where
+  Eq15 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2, o2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2 && l1 == l2 && m1 == m2 && n1 == n2 && o1 == o2
+
+-- these all look to be overlapping, but they are differentiated by their kinds
+type instance a == b = EqStar a b
+type instance a == b = EqArrow a b
+type instance a == b = EqBool a b
+type instance a == b = EqOrdering a b
+type instance a == b = EqUnit a b
+type instance a == b = EqList a b
+type instance a == b = EqMaybe a b
+type instance a == b = Eq2 a b
+type instance a == b = Eq3 a b
+type instance a == b = Eq4 a b
+type instance a == b = Eq5 a b
+type instance a == b = Eq6 a b
+type instance a == b = Eq7 a b
+type instance a == b = Eq8 a b
+type instance a == b = Eq9 a b
+type instance a == b = Eq10 a b
+type instance a == b = Eq11 a b
+type instance a == b = Eq12 a b
+type instance a == b = Eq13 a b
+type instance a == b = Eq14 a b
+type instance a == b = Eq15 a b
index e88fc31..41607c3 100644 (file)
@@ -8,6 +8,7 @@
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UndecidableInstances #-}  -- for compiling instances of (==)
 {-# OPTIONS_GHC -XNoImplicitPrelude #-}
 {-| This module is an internal GHC module.  It declares the constants used
 in the implementation of type-level natural numbers.  The programmer interface
@@ -31,7 +32,7 @@ module GHC.TypeLits
 
   ) where
 
-import GHC.Base(Eq(..), Ord(..), Bool(True), otherwise)
+import GHC.Base(Eq(..), Ord(..), Bool(True,False), otherwise)
 import GHC.Num(Integer)
 import GHC.Base(String)
 import GHC.Show(Show(..))
@@ -39,6 +40,7 @@ import GHC.Read(Read(..))
 import GHC.Prim(magicDict)
 import Data.Maybe(Maybe(..))
 import Data.Proxy(Proxy(..))
+import Data.Type.Equality(type (==))
 
 -- | (Kind) This is the kind of type-level natural numbers.
 data Nat
@@ -115,6 +117,15 @@ instance Show SomeSymbol where
 instance Read SomeSymbol where
   readsPrec p xs = [ (someSymbolVal a, ys) | (a,ys) <- readsPrec p xs ]
 
+type family EqNat (a :: Nat) (b :: Nat) where
+  EqNat a a = True
+  EqNat a b = False
+type instance a == b = EqNat a b
+
+type family EqSymbol (a :: Symbol) (b :: Symbol) where
+  EqSymbol a a = True
+  EqSymbol a b = False
+type instance a == b = EqSymbol a b
 
 --------------------------------------------------------------------------------