-- 4) Class declarations: @class Foo where@ creates the @Foo@ type constructor of kind @*@
--
-- 5) Type coercions! This is because we represent a coercion from @t1@ to @t2@ as a 'Type', where
--- that type has kind @t1 :=: t2@. See "Coercion" for more on this
+-- that type has kind @t1 ~ t2@. See "Coercion" for more on this
--
-- This data type also encodes a number of primitive, built in type constructors such as those
-- for function and tuple types.
algTcRec :: RecFlag, -- ^ Tells us whether the data type is part of a mutually-recursive group or not
- hasGenerics :: Bool, -- ^ Whether generic (in the -XGenerics sense) to/from functions are
+ hasGenerics :: Bool, -- ^ Whether generic (in the -XGenerics sense) to\/from functions are
-- available in the exports of the data type's source module.
algTcParent :: TyConParent -- ^ Gives the class or family declaration 'TyCon' for derived 'TyCon's
tyConExtName :: Maybe FastString -- ^ @Just e@ for foreign-imported types, holds the name of the imported thing
}
- -- | Type coercions, such as @(:=:)@, @sym@, @trans@, @left@ and @right@.
+ -- | Type coercions, such as @(~)@, @sym@, @trans@, @left@ and @right@.
-- INVARIANT: coercions are always fully applied
| CoercionTyCon {
tyConUnique :: Unique,
newtype T a = MkT (a -> a)
-the NewTyCon for T will contain nt_co = CoT where CoT t : T t :=: t ->
+the NewTyCon for T will contain nt_co = CoT where CoT t : T t ~ t ->
t. This TyCon is a CoercionTyCon, so it does not have a kind on its
own; it basically has its own typing rule for the fully-applied
version. If the newtype T has k type variables then CoT has arity at
newtype S a = MkT [a]
-then we would generate the arity 0 coercion CoS : S :=: []. The
+then we would generate the arity 0 coercion CoS : S ~ []. The
primary reason we do this is to make newtype deriving cleaner.
In the paper we'd write
- axiom CoT : (forall t. T t) :=: (forall t. [t])
+ axiom CoT : (forall t. T t) ~ (forall t. [t])
and then when we used CoT at a particular type, s, we'd say
CoT @ s
which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s])
TyConApp CoT [s]
In the vocabulary of the paper it's as if we had axiom declarations
like
- axiom CoT t : T t :=: [t]
+ axiom CoT t : T t ~ [t]
Note [Newtype eta]
~~~~~~~~~~~~~~~~~~
\end{code}
\begin{code}
--- | Does this 'TyCon' have any generic to/from functions available? See also 'hasGenerics'
+-- | Does this 'TyCon' have any generic to\/from functions available? See also 'hasGenerics'
tyConHasGenerics :: TyCon -> Bool
tyConHasGenerics (AlgTyCon {hasGenerics = hg}) = hg
tyConHasGenerics (TupleTyCon {hasGenerics = hg}) = hg