Skip to content

Instantly share code, notes, and snippets.

@goldfirere
Created January 30, 2016 19:34
Show Gist options
  • Save goldfirere/846c3faf7640e27025f0 to your computer and use it in GitHub Desktop.
Save goldfirere/846c3faf7640e27025f0 to your computer and use it in GitHub Desktop.
TypeRep tomfoolery
{-# LANGUAGE TypeOperators, TypeFamilies, TypeApplications,
ExplicitForAll, ScopedTypeVariables, GADTs, TypeFamilyDependencies,
TypeInType, ConstraintKinds, UndecidableInstances,
FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies,
FlexibleContexts, StandaloneDeriving, InstanceSigs #-}
module Basics where
import Data.Type.Bool
import Data.Type.Equality
import GHC.TypeLits
import Data.Proxy
import GHC.Exts
import Data.Kind
import Data.Functor.Compose
data (a :: k1) :~~: (b :: k2) where
HRefl :: a :~~: a
data Dict :: Constraint -> Type where
Dict :: c => Dict c
-- Type-level inequality
type a /= b = Not (a == b)
-- append two schemas
type family s1 ++ s2 where
'[] ++ s2 = s2
(s ': s1) ++ s2 = s ': (s1 ++ s2)
natValue :: forall n. KnownNat n => Integer
natValue = natVal @n Proxy
type family All c tys where
All _ '[] = (() :: Constraint)
All c (ty ': tys) = (c ty, All c tys)
type family Sing = (r :: k -> Type) | r -> k
data SList :: forall k. [k] -> Type where
SNil :: SList '[]
SCons :: Sing h -> SList t -> SList (h ': t)
type instance Sing = SList
data TypeRep (a :: k) where
TyCon :: Primitive a => TyCon a -> TypeRep a
TyApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
type family Primitive (a :: k) :: Constraint where
Primitive (_ _) = (False ~ True) -- TypeError (ShowType (a b) :<>: Text " is not primitive")
Primitive _ = (() :: Constraint)
data TyCon (a :: k) where
Int :: TyCon Int
Bool :: TyCon Bool
Char :: TyCon Char
List :: TyCon []
Maybe :: TyCon Maybe
Arrow :: TyCon (->)
TYPE :: TyCon TYPE
Levity :: TyCon Levity
Lifted' :: TyCon 'Lifted
Unlifted' :: TyCon 'Unlifted
-- add to eqTyCon too
eqTyCon :: TyCon a -> TyCon b -> Maybe (a :~~: b)
eqTyCon Int Int = Just HRefl
eqTyCon Bool Bool = Just HRefl
eqTyCon Char Char = Just HRefl
eqTyCon List List = Just HRefl
eqTyCon Maybe Maybe = Just HRefl
eqTyCon Arrow Arrow = Just HRefl
eqTyCon TYPE TYPE = Just HRefl
eqTyCon Levity Levity = Just HRefl
eqTyCon Lifted' Lifted' = Just HRefl
eqTyCon Unlifted' Unlifted' = Just HRefl
eqTyCon _ _ = Nothing
tcType :: TypeRep Type
tcType = TyApp (TyCon TYPE) (TyCon Lifted')
data TypeRepX :: (forall k. k -> Constraint) -> Type where
TypeRepX :: forall k (c :: forall k'. k' -> Constraint) (a :: k).
c a => TypeRep a -> TypeRepX c
-- TypeRepX ((~~) Type)
-- (~~) :: forall k1 k2. k1 -> k2 -> Constraint
-- I need: (~~) :: forall k1. k1 -> forall k2. k2 -> Constraint
data TyConX where
TyConX :: Primitive a => TyCon a -> TyConX
instance Read TyConX where
readsPrec _ "Int" = [(TyConX Int, "")]
readsPrec _ "Bool" = [(TyConX Bool, "")]
readsPrec _ _ = []
class ConstTrue (a :: k) -- RAE: needs the :: k to make it a specified tyvar
instance ConstTrue a
instance Read (TypeRepX ConstTrue) where
readsPrec _ "String" = [(TypeRepX (typeRep @String), "")]
readsPrec p s = case readsPrec p s of
[(TyConX tc, "")] -> [(TypeRepX (TyCon tc), "")]
_ -> []
-- instance Read (TypeRepX ((~~) Type)) RAE: need (~~) :: forall k1. k1 -> forall k2. k2 -> Constraint
-- RAE: need kind signatures on classes
class k ~~ Type => IsType (x :: k)
instance k ~~ Type => IsType (x :: k)
eqT :: TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqT (TyCon tc1) (TyCon tc2) = eqTyCon tc1 tc2
eqT (TyApp f1 a1) (TyApp f2 a2) = do
HRefl <- eqT f1 f2
HRefl <- eqT a1 a2
return HRefl
eqT _ _ = Nothing
instance Read (TypeRepX IsType) where
readsPrec p s = case readsPrec @(TypeRepX ConstTrue) p s of
[(TypeRepX tr, "")]
| Just HRefl <- eqT (kindRep tr) tcType
-> [(TypeRepX tr, "")]
_ -> error "wrong kind"
type instance Sing = (TypeRep :: Type -> Type)
data SSymbol :: Symbol -> Type where
SSym :: KnownSymbol s => SSymbol s
type instance Sing = SSymbol
kindRep :: TypeRep (a :: k) -> TypeRep k
kindRep (TyCon tc) = tcKindRep tc
kindRep (TyApp (f :: TypeRep (tf :: k1 -> k)) _) = case kindRep f :: TypeRep (k1 -> k) of
TyApp _ res -> res
tcArrow :: TypeRep (->)
tcArrow = TyCon Arrow
mkFunTy :: TypeRep a -> TypeRep b -> TypeRep (a -> b)
mkFunTy arg res = tcArrow `TyApp` arg `TyApp` res
infixr 0 `mkFunTy`
tcKindRep :: TyCon (a :: k) -> TypeRep k
tcKindRep Int = tcType
tcKindRep Bool = tcType
tcKindRep Char = tcType
tcKindRep List = mkFunTy tcType tcType
tcKindRep Maybe = mkFunTy tcType tcType
tcKindRep Arrow = tcType `mkFunTy` tcType `mkFunTy` tcType
tcKindRep TYPE = TyCon Levity `mkFunTy` tcType
tcKindRep Unlifted' = TyCon Levity
tcKindRep Lifted' = TyCon Levity
tcKindRep Levity = tcType
class TyConAble a where
tyCon :: TyCon a
instance TyConAble Int where tyCon = Int
instance TyConAble Bool where tyCon = Bool
instance TyConAble Char where tyCon = Char
instance TyConAble [] where tyCon = List
instance TyConAble Maybe where tyCon = Maybe
instance TyConAble (->) where tyCon = Arrow
instance TyConAble TYPE where tyCon = TYPE
instance TyConAble 'Unlifted where tyCon = Unlifted'
instance TyConAble 'Lifted where tyCon = Lifted'
instance TyConAble Levity where tyCon = Levity
type family CheckPrim a where
CheckPrim (_ _) = 'False
CheckPrim _ = 'True
class Typeable' a (b :: Bool) where
typeRep' :: TypeRep a
type Typeable a = Typeable' a (CheckPrim a)
instance (Primitive a, TyConAble a) => Typeable' a 'True where
typeRep' = TyCon tyCon
instance (Typeable a, Typeable b) => Typeable' (a b) 'False where
typeRep' = TyApp typeRep typeRep
typeRep :: forall a. Typeable a => TypeRep a
typeRep = typeRep' @_ @_ @(CheckPrim a) -- RAE: #11512 says we need the extra @_.
instance Show (TypeRep a) where
show (TyCon tc) = show tc
show (TyApp tr1 tr2) = show tr1 ++ " " ++ show tr2
deriving instance Show (TyCon a)
instance TestEquality SSymbol where
testEquality :: forall s1 s2. SSymbol s1 -> SSymbol s2 -> Maybe (s1 :~: s2)
testEquality SSym SSym = sameSymbol @s1 @s2 Proxy Proxy
instance TestEquality TypeRep where
testEquality tr1 tr2
| Just HRefl <- eqT tr1 tr2
= Just Refl
| otherwise
= Nothing
instance Show (SSymbol name) where
show s@SSym = symbolVal s
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment