From 111bc9a9a9bd0ae96b0ee1e261abac4ddd48c0e1 Mon Sep 17 00:00:00 2001 From: "simonpj@microsoft.com" Date: Sat, 17 Apr 2010 14:50:32 +0000 Subject: [PATCH] Comments only (about type families) --- compiler/types/TyCon.lhs | 117 +++++++++++++++++++++++++++++++++++++++------- 1 file changed, 100 insertions(+), 17 deletions(-) diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs index 340ccba..507bff5 100644 --- a/compiler/types/TyCon.lhs +++ b/compiler/types/TyCon.lhs @@ -100,6 +100,87 @@ import qualified Data.Data as Data import Data.List( elemIndex ) \end{code} +----------------------------------------------- + Notes about type families +----------------------------------------------- + +Type synonym families +~~~~~~~~~~~~~~~~~~~~~~ +* Type synonym families, also known as "type functions", map directly + onto the type functions in FC: + + type family F a :: * + type instance F Int = Bool + ..etc... + +* From the user's point of view (F Int) and Bool are simply equivalent + types. + +* A Haskell 98 type synonym is a degenerate form of a type synonym + family. + +* Type functions can't appear in the LHS of a type function: + type instance F (F Int) = ... -- BAD! + +* In the future we might want to support + * closed type families (esp when we have proper kinds) + * injective type families (allow decomposition) + but we don't at the moment [2010] + +Data type families +~~~~~~~~~~~~~~~~~~ +* Data type families are declared thus + data family T a :: * + data instance T Int = T1 | T2 Bool + data instance T [a] where + X1 :: T [Int] + X2 :: a -> T [a] + +* The user does not see any "equivalent types" as he did with type + synonym families. He just sees constructors with types + T1 :: T Int + T2 :: Bool -> T Int + X1 :: T [Int] + X2 :: a -> T [a] + Note that X2 is a fully-fledged GADT constructor; that's fine + +* The conversion into FC is interesting, and is the point where I was + getting mixed up. Here's the FC version of the above declarations: + + data T a + data TI = T1 | T2 Bool + axiom ax_ti : T Int ~ TI + + data TL a where + X1 :: TL Int + X2 :: a -> TL a + axiom ax_tl :: T [a] ~ TL a + +* Notice that T is NOT translated to a FC type function; it just + becomes a "data type" with no constructors, into which TI, TL, TB + are cast using their respective axioms. + +* As a result + - T behaves just like a data type so far as decomposition is concerned + - It's fine to have T in the LHS of a type function: + type instance F (T a) = [a] + +It was this last point that confused me! The big thing is that you +should not think of a data family T as a *type function* at all, not +even an injective one! We can't allow even injective type functions +on the LHS of a type function: + type family injective G a :: * + type instance F (G Int) = Bool +is no good, even if G is injective, because consider + type instance G Int = Bool + type instance F Bool = Char + +So a data type family is not an injective type function. It's just a +data type with some axioms that connect it to other data types. These +axioms come into play when (and only when) you + - use a data constructor + - do pattern matching + %************************************************************************ %* * \subsection{The data type} @@ -365,17 +446,11 @@ data TyConParent -- -- 3) A 'CoTyCon' identifying the representation -- type with the type instance family - | FamilyTyCon + | FamilyTyCon -- See Note [Data type families] TyCon [Type] TyCon -- c.f. Note [Newtype coercions] - -- - -- E.g. data intance T [a] = ... - -- gives a representation tycon: - -- data :R7T a = ... - -- axiom co a :: T [a] ~ :R7T a - -- with :R7T's algTcParent = FamilyTyCon T [a] co -- | Checks the invariants of a 'TyConParent' given the appropriate type class name, if any okParent :: Name -> TyConParent -> Bool @@ -485,34 +560,42 @@ so the coercion tycon CoT must have and arity: 0 -Note [Indexed data types] (aka data type families) -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - See also Note [Wrappers for data instance tycons] in MkId.lhs +Note [Data type families] +~~~~~~~~~~~~~~~~~~~~~~~~~ +See also Note [Wrappers for data instance tycons] in MkId.lhs Consider data family T a data instance T (b,c) where T1 :: b -> c -> T (b,c) + T2 :: T (Int,Bool) + +Notice that the 'data instance' can be a fully-fledged GADT -Then - * T is the "family TyCon" + * T is the "family TyCon". It is a data type + whose AlgTyConRhs is OpenTyCon - * We make "representation TyCon" :R1T, thus: + * For each 'data instance' we make "representation TyCon" + :R1T, thus: data :R1T b c where T1 :: forall b c. b -> c -> :R1T b c + T1 :: :R1T Int Bool + We have a bit of work to do, to unpick the result types of the + data instance declaration to get the result type in the + representation; e.g. T (Int,Bool) --> :R1T Int Bool - * It has a top-level coercion connecting it to the family TyCon + * We defind a top-level coercion connecting it to the family TyCon axiom :Co:R1T b c : T (b,c) ~ :R1T b c - * The data contructor T1 has a wrapper (which is what the source-level - "T1" invokes): + * The data contructor T1 has a wrapper (which is what the + source-level "T1" invokes): $WT1 :: forall b c. b -> c -> T (b,c) $WT1 b c (x::b) (y::c) = T1 b c x y `cast` sym (:Co:R1T b c) - * The representation TyCon :R1T has an AlgTyConParent of + * The representation TyCon, :R1T, has an AlgTyConParent of FamilyTyCon T [(b,c)] :Co:R1T -- 1.7.10.4