Data.PolyKinded.Atom

Atoms represent the shape of a type, possibly with variables, which can be Interpreted given a list of types.

Atoms

data Atom (d :: Type) (k :: TYPE r) where

Shape of a type, possibly with type variables.

>>> :kind Kon [] :@: Var0 -- the type [a] for unknown a
Kon [] :@: Var0 :: Atom (* -> xs) *

Representation of type families

Type families are represented using first-class-families.

For example, the type-level n + m :: Nat-- may expand to the following--

n + m         -- using (+) from GHC.TypeNats
~
Eval (n + m)  -- using Eval from Fcf.Core and (+) from Fcf.Data.Nat

which may be encoded as the following Atom (using Var0 for n and Var1 for m):

Eval ((Kon (+) :@: Var0) :@: Var1)  -- Eval as Atom's constructor
  :: Atom (Nat -> Nat -> Type) Nat

kind-generics uses a different, more systematic encoding of type families for GenericK instances; see fcf-family for more details. For example, n + m is instead expanded to the following:

n + m
~
Eval (NDFamily (MkName "base" "GHC.TypeNats" "+") P0 '(n, '(m, '())))

which gets encoded as the following Atom:

Eval (Kon (NDFamily (MkName "base" "GHC.TypeNats" "+") P0)
        :@: ((Kon '(,) :@: Var0) :@: ((Kon '(,) :@: Var1) :@: Kon '())))
  :: Atom (Nat -> Nat -> Type) Nat

Constructors

Var :: TyVar d k -> Atom d k

Represents a type variable.

Kon :: k -> Atom d k

Represents a constant type, like Int.

(:@:) :: Atom d (k1 -> k2) -> Atom d k1 -> Atom d k2

Represents type application.

(:&:) :: Atom d Constraint -> Atom d Constraint -> Atom d Constraint infixr 5

Represents the conjunction of two constraints.

ForAll :: Atom (d1 -> d) Type -> Atom d Type

Represents universal quantification.

(:=>>:) :: Atom d Constraint -> Atom d Type -> Atom d Type infixr 5

Represents constraint requirement, the "thick arrow" =>.

Eval :: Atom d (Exp k) -> Atom d k

Represents a type family application.

type (:$:) f x = 'Kon f :@: x

Represents an applied constructor. Instead of Kon [] :: Var0$ you can write @[] :$: Var0$.

type (:~:) a b = ('Kon (~) :@: a) :@: b

Represents (homogeneous) type equality.

type (:~~:) a b = ('Kon (~~) :@: a) :@: b

Represents heterogeneous type equality.

Type variables

data TyVar (d :: Type) (k :: TYPE r) where

Well-scoped de Bruijn representation of type variables. TyVar d represents all the possible type variables which can refer to the holes in kind d.

We recommend using the aliases Var0, Var1, ... instead of the constructors, for further clarity.

Constructors

VZ :: TyVar (x -> xs) x

First hole in d.

VS :: TyVar xs k -> TyVar (x -> xs) k

Successor hole, increases the hole reference by 1.

Aliases for specific variables

type Var0 = 'Var 'VZ

type Var1 = 'Var ('VS 'VZ)

type Var2 = 'Var ('VS ('VS 'VZ))

type Var3 = 'Var ('VS ('VS ('VS 'VZ)))

type Var4 = 'Var ('VS ('VS ('VS ('VS 'VZ))))

type Var5 = 'Var ('VS ('VS ('VS ('VS ('VS 'VZ)))))

type Var6 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS 'VZ))))))

type Var7 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ)))))))

type Var8 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ))))))))

type Var9 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ)))))))))

Intepretation

type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where ...

Replaces the holes in the Atom t by the elements of the list of types tys. The amount and kind of types in tys must match statically those required by the Atom.

>>> :kind! Interpret ([] :$: Var0) (LoT1 Int)
Interpret ([] :$: Var0) (LoT1 Int) :: *
= [Int]

Equations

Interpret ('Var v) tys = InterpretVar v tys

Interpret ('Kon t) tys = t

Interpret (f :@: x) tys = Interpret f tys (Interpret x tys)

Interpret (c :&: d) tys = (Interpret c tys, Interpret d tys)

Interpret ('ForAll f) tys = ForAllI f tys

Interpret (c :=>>: f) tys = SuchThatI c f tys

Interpret ('Eval f) tys = Eval (Interpret f tys)

type family InterpretVar (t :: TyVar d k) (tys :: LoT d) :: k where ...

Obtains the type in the list tys referenced by the type variable t.

>>> :kind! Interpret Var0 (LoT2 Int Bool)
Interpret Var0 (LoT2 Int Bool) :: *
= Int
>>> :kind! Interpret Var1 (LoT2 Int Bool)
Interpret Var1 (LoT2 Int Bool) :: *
= Bool

Equations

InterpretVar 'VZ tys = HeadLoT tys

InterpretVar ('VS v) tys = InterpretVar v (TailLoT tys)

type family Satisfies (cs :: [Atom d Constraint]) (tys :: LoT d) :: Constraint where ...

Interprets a list of Atom representing constraints into the actual constraints. This is a specialization of Interpret for the case of constraints.

>>> :kind! Satisfies '[Eq :$: Var0, Show :$: Var0] (LoT1 Int)
Satisfies '[Eq :$: Var0, Show :$: Var0] (LoT1 Int) :: Constraint
= (Eq Int, (Show Int, () :: Constraint))

Equations

Satisfies '[] tys = ()

Satisfies (c ': cs) tys = (Interpret c tys, Satisfies cs tys)

type family ContainsTyVar (v :: TyVar d k) (t :: Atom d p) :: Bool where ...

Determines whether a given type variable v is used within an Atom t. If not, we know that the atom is constant with respect to that variable.

Equations

ContainsTyVar v ('Var v) = 'True

ContainsTyVar v ('Var w) = 'False

ContainsTyVar v ('Kon t) = 'False

ContainsTyVar v (f :@: x) = Or (ContainsTyVar v f) (ContainsTyVar v x)

ContainsTyVar v (x :&: y) = Or (ContainsTyVar v x) (ContainsTyVar v y)

ContainsTyVar v (c :=>>: f) = Or (ContainsTyVar v c) (ContainsTyVar v f)

ContainsTyVar v ('ForAll f) = ContainsTyVar ('VS v) f

Auxiliary types for interpretation

newtype ForAllI (f :: Atom (d1 -> d) Type) (tys :: LoT d) where

Auxiliary type for interpretation of the ForAll atom. Required because a type family like Interpret cannot return a polymorphic type.

Constructors

ForAllI :: (forall t. Interpret f (t :&&: tys)) -> ForAllI f tys

newtype SuchThatI (c :: Atom d Constraint) (f :: Atom d Type) (tys :: LoT d) where

Auxiliary type for interpretation of the (:=>>:) atom. Required because a type family like Interpret cannot return a type with constraints.

Constructors

SuchThatI

Fields

• :: { unSuchThatI :: Interpret c tys => Interpret f tys
•    } -> SuchThatI c f tys

Records a type as constructor + list of variables

newtype WrappedI (f :: Atom d Type) (tys :: LoT d)

Records a value of type f applied to the list tys.

>>> :t WrapI [1] :: WrappedI ([] :$: Var0) (LoT1 Int)
WrapI [1] :: WrappedI ([] :$: Var0) (LoT1 Int)

Constructors

WrapI

Fields

• unwrapI :: Interpret f tys

toWrappedI :: forall f tys t. ForAllI f tys -> WrappedI f (t :&&: tys)

fromWrappedI :: forall f tys. (forall t. WrappedI f (t :&&: tys)) -> ForAllI f tys