Skip to content

Changes

Page history
Edit Typeable authored by bgamari's avatar bgamari
Hide whitespace changes
Inline Side-by-side
typeable.md
View page @ 81ebcad2
......@@ -17,23 +17,22 @@ See also
Consider `Dynamic`:
```wiki
data Dynamic where
Dyn :: TypeRep -> a -> Dynamic
```
dataDynamicwhereDyn::TypeRep-> a ->Dynamic
```
We'd like to write `dynApply`:
```wiki
dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
```
dynApply::Dynamic->Dynamic->MaybeDynamic
```
which succeeds only when the application is type correct. But how? Let's try
```wiki
dynApply (Dyn tf f) (Dyn tx x) = ???
```
dynApply(Dyn tf f)(Dyn tx x)=???
```
......@@ -42,10 +41,8 @@ We need some way to decompose `tf` (the type representation for `f`), ask if it
But at the moment we don't have any *type-safe* way to decompose `TypeRep`. Indeed `dynApply` is defined like this right now:
```wiki
dynApply (Dyn tf f) (Dyn tx x)
= case funResultTy tf tx of
Just tr -> Just (Dyn tr (unsafeCoerce f x))
```
dynApply(Dyn tf f)(Dyn tx x)=case funResultTy tf tx ofJust tr ->Just(Dyn tr (unsafeCoerce f x))
```
......@@ -64,9 +61,8 @@ So **our main goal is to be able to write `dynApply` in a type-safe way** so tha
The first obvious thing is that we must make a connection between the type-rep arg of `Dyn` and the value itself. Something like this:
```wiki
data Dynamic where
Dyn :: TTypeRep a -> a -> Dynamic
```
dataDynamicwhereDyn::TTypeRep a -> a ->Dynamic
```
......@@ -75,16 +71,9 @@ Here we are using a *type-indexed* type representation, `TTypeRep`. Now the con
We can re-define the `Typeable` class and `TypeRep` thus:
```wiki
class Typeable a where
tTypeRep :: TTypeRep a -- No need for a proxy argument!
data TypeRep where
TypeRep :: TTypeRep a -> TypeRep
typeRep :: Typeable a => proxy a -> TypeRep
-- The current typeRep function
typeRep (p :: proxy a) = TypeRep (tTypeRep :: TTypeRep a)
```
classTypeable a where
tTypeRep ::TTypeRep a -- No need for a proxy argument!dataTypeRepwhereTypeRep::TTypeRep a ->TypeReptypeRep::Typeable a => proxy a ->TypeRep-- The current typeRep functiontypeRep(p :: proxy a)=TypeRep(tTypeRep ::TTypeRep a)
```
......@@ -97,8 +86,8 @@ It is helpful to have both `Typeable a` (the class) and `TTypeRep a` (the value)
We can get from `Typeable a` to `TTypeRep` by using the class method `tTypeRep`. But what about the other way round?
We need to add the following primitive:
```wiki
withTypeable :: TTypeRep a -> (Typeable a => b) -> b
```
withTypeable::TTypeRep a ->(Typeable a => b)-> b
```
......@@ -107,12 +96,8 @@ withTypeable :: TTypeRep a -> (Typeable a => b) -> b
We can also compare two `TTypeReps` to give a statically-usable proof of equality:
```wiki
eqTT :: TTypeRep a -> TTypeRep b -> Maybe (a :~: b)
eqT :: (Typeable a, Typeable b) => Maybe (a :~: b)
data a :~: b where -- Defined in Data.Typeable.Equality
Refl :: a :~: a
```
eqTT::TTypeRep a ->TTypeRep b ->Maybe(a :~: b)eqT::(Typeable a,Typeable b)=>Maybe(a :~: b)data a :~: b where-- Defined in Data.Typeable.EqualityRefl:: a :~: a
```
......@@ -125,15 +110,11 @@ data a :~: b where -- Defined in Data.Typeable.Equality
If we want to decompose `TTypable`, at least in the function arrow case, we need a function like this:
```wiki
decomposeFun :: TTypeRep fun
-> r
-> (forall arg res. (fun ~ (arg->res))
=> TTypeRep arg -> TTypeRep res -> r)
```
decomposeFun::TTypeRep fun
-> r
-- (decomposeFun tf def k) sees if 'tf' is a function type
-- If so, it applies 'k' to the argument and result type
-- representations; if not, it returns 'def'
->(forall arg res.(fun ~(arg->res))=>TTypeRep arg ->TTypeRep res -> r)-> r
-- (decomposeFun tf def k) sees if 'tf' is a function type-- If so, it applies 'k' to the argument and result type-- representations; if not, it returns 'def'
```
......@@ -142,34 +123,23 @@ This function is part of `Typeable`, and replaces `funResultTy`.
Now we can write `dynApply`, in a completely type-safe way, outside the TCB:
```wiki
dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
dynApply (Dyn tf f) (Dyn tx x)
= decomposeFun tf Nothing $ \ ta tr ->
case eqTT ta tx of
Nothing -> Nothing
Just Refl -> Just (Dyn tr (f x))
```
dynApply::Dynamic->Dynamic->MaybeDynamicdynApply(Dyn tf f)(Dyn tx x)= decomposeFun tf Nothing$\ ta tr ->case eqTT ta tx ofNothing->NothingJustRefl->Just(Dyn tr (f x))
```
**Pattern synonyms**. An alternative, rather nicer interface for `decomoposeFun` would use a [pattern synonym](pattern-synonyms) instead of continuation-passing style. Here is the signature for the pattern synonym:
```wiki
pattern TRFun :: fun ~ (arg -> res)
=> TTypeRep arg
-> TTypeRep res
-> TTypeRep fun
```
patternTRFun:: fun ~(arg -> res)=>TTypeRep arg
->TTypeRep res
->TTypeRep fun
```
which looks (by design) very like the signature for a GADT data constructor. Now we can use `TRFun` in a pattern, thus:
```wiki
dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
dynApply (Dyn (TRFun ta tr) f) (Dyn tx x)
= case eqTT ta tx of
Nothing -> Nothing
Just Refl -> Just (Dyn tr (f x))
dynApply _ _ = Nothing
```
dynApply::Dynamic->Dynamic->MaybeDynamicdynApply(Dyn(TRFun ta tr) f)(Dyn tx x)=case eqTT ta tx ofNothing->NothingJustRefl->Just(Dyn tr (f x))dynApply__=Nothing
```
......@@ -183,8 +153,8 @@ Is that not beautiful? The second equation for `dynApply` is needed in case the
Suppose we have a `TTypeRep (a :: k)`. It might be nice to get a `TTypeRep (k :: *)`
out of it. (Here, we assume `* :: *`, but the idea actually works without that assumption.) An example is an attempt to typecheck the *expression*
```wiki
typeOf :: Typeable (a :: k) => Proxy a -> TypeRep
```
typeOf::Typeable(a :: k)=>Proxy a ->TypeRep
```
......@@ -193,8 +163,8 @@ where `typeOf :: Typeable a => a -> TypeRep` is a long-standing part of the `Typ
So, we now include
```wiki
kindRep :: TTypeRep (a :: k) -> TTypeRep k
```
kindRep::TTypeRep(a :: k)->TTypeRep k
```
......@@ -210,14 +180,10 @@ It is all very well being able to decompose functions, but what about decomposin
To do this it is natural to regard types as built from type constructors and binary application, like this:
```wiki
data TTypeRep (a :: k) :: * where
TRApp :: TTypeRep a -> TTypeRep b -> TTypeRep (a b)
TRCon :: TTyCon a -> TTypeRep a
```
dataTTypeRep(a :: k)::*whereTRApp::TTypeRep a ->TTypeRep b ->TTypeRep(a b)TRCon::TTyCon a ->TTypeRep a
-- TTyCon must be polykinded, so that we can have
-- (TTyCon Maybe), (TTyCon Either), (TTyCon Int) etc
-- TTyCon :: forall k. k -> *
-- TTyCon must be polykinded, so that we can have-- (TTyCon Maybe), (TTyCon Either), (TTyCon Int) etc-- TTyCon :: forall k. k -> *
```
......@@ -226,48 +192,39 @@ data TTypeRep (a :: k) :: * where
While this GADT is expressible in GHC now (note the existential kind in TRApp), **it is not very useful without kind equalities**. (GHC does not currently support kind equalities, but Richard Eisenberg is working that very question.) Why? Here is the type of `TRApp` in its full glory, with normally-invisible kind args in angle brackets:
```wiki
TRApp :: forall k1 k2. forall (a :: k1 -> k2) (b :: k1).
TTypeRep <k1->k2> a -> TTypeRep <k1> b -> TTypeRep <k2> (a b)
```
TRApp:: forall k1 k2. forall (a :: k1 -> k2)(b :: k1).TTypeRep<k1->k2> a ->TTypeRep<k1> b ->TTypeRep<k2>(a b)
```
Or, to be really explicit about the existentials:
```wiki
TRApp :: forall k2 (c:k2). -- Universal
forall k1 (a :: k1 -> k2) (b :: k1). -- Existential
(c ~ a b)
=> TTypeRep <k1->k2> a
-> TTypeRep <k2> b
-> TTypeRep <k2> c
```
TRApp:: forall k2 (c:k2).-- Universal
forall k1 (a :: k1 -> k2)(b :: k1).-- Existential(c ~ a b)=>TTypeRep<k1->k2> a
->TTypeRep<k2> b
->TTypeRep<k2> c
```
Now suppose we want to implement `decomposeFun`. We should be able to do this outside the TCB, i.e. without `unsafeCoerce`:
```wiki
arrowCon :: TTyCon (->) -- The type rep for (->)
decomposeFun :: TTypeRep fun
-> r
-> (forall arg res. (fun ~ (arg->res))
=> TypeRep arg -> TTypeRep res -> r)
```
arrowCon::TTyCon(->)-- The type rep for (->)decomposeFun::TTypeRep fun
-> r
->(forall arg res.(fun ~(arg->res))=>TypeRep arg ->TTypeRep res -> r)-> r
decomposeFun tr def kont
= case tr of
TRApp (TRApp (TRCon c) r1) r2 -> case eqTyCon arrowCon c of
Just HRefl -> kont r1 r2
Nothing -> def
_ -> default
=case tr ofTRApp(TRApp(TRCon c) r1) r2 ->case eqTyCon arrowCon c ofJustHRefl-> kont r1 r2
Nothing-> def
_->default
```
But look at the arguments of `eqTyCon`:
```wiki
arrowCon :: TTyCon <*->*->*> (->)
c :: TTyCon <k1->k2->*> tc
```
arrowCon ::TTyCon<*->*->*>(->)
c ::TTyCon<k1->k2->*> tc
```
......@@ -276,27 +233,23 @@ where `k1` and `k2` are existential kinds bound by the two nested `TRApp` constr
The real work is done by `eqTyCon`:
```wiki
eqTyCon :: forall (k1 k2 :: *).
forall (a :: k1) (b :: k2).
TTyCon <k1> a -> TTyCon <k2> b -> Maybe (a :~~: b)
```
eqTyCon:: forall (k1 k2 ::*).
forall (a :: k1)(b :: k2).TTyCon<k1> a ->TTyCon<k2> b ->Maybe(a :~~: b)
```
where `:~~:` is a *kind-heterogeneous* version of `:~:`:
```wiki
data (a::k1) :~~: (b::k2) where
HRefl :: forall (a::k). a :~~: a
```
data(a::k1):~~:(b::k2)whereHRefl:: forall (a::k). a :~~: a
```
Or, to write the type of `HRefl` with its constraints explicit:
```wiki
HRefl :: forall k1 k2. forall (a::k1) (b::k2).
(k1 ~ k2, a ~ b)
=> a :~~: b
```
HRefl:: forall k1 k2. forall (a::k1)(b::k2).(k1 ~ k2, a ~ b)=> a :~~: b
```
......@@ -322,11 +275,8 @@ Conclusion: make `TypeRep` abstract. But then how can we pattern-match on it?
With all of this, what is left in the TCB? The `TTyCon` type is a new abstract type, and the comparison (based on fingerprints) must be in the TCB.
```wiki
TTyCon a --- abstract type
eqTyCon :: forall k1 k2. forall (a :: k1) (b :: k2).
TTyCon a -> TTyCon b -> Maybe (a :~~: b)
tyConKind :: TTyCon (a :: k) -> TTypeRep (k :: *)
```
TTyCon a --- abstract typeeqTyCon:: forall k1 k2. forall (a :: k1)(b :: k2).TTyCon a ->TTyCon b ->Maybe(a :~~: b)tyConKind::TTyCon(a :: k)->TTypeRep(k ::*)
```
......@@ -334,8 +284,8 @@ Note that `TTyCon` represents type constructors already applied to any kind argu
`withTypeable` could be written in core (and perhaps could be generalized to other constraints) but not in source Haskell:
```wiki
withTypeable :: TypeRep a -> (Typeable a => b) -> b
```
withTypeable::TypeRep a ->(Typeable a => b)-> b
```
......@@ -362,69 +312,28 @@ implementation of `decomposeFun` will use `unsafeCoerce` and will be part of the
This version assumes homoegeneous equality (as GHC is today, July 2, 2015). Below is the version with heterogeneous equality.
```wiki
data TTypeRep (a :: k) -- abstract
data TTyCon (a :: k) -- abstract
-- Costructors
trCon :: forall k (a :: k). TTyCon a -> TTypeRep a -- in TCB
trApp :: forall k k1 (a :: k1 -> k) (b :: k1).
TTypeRep a -> TTypeRep b -> TTypeRep (a b) -- in TCB
-- Destructors
pattern type TRCon :: forall k (a :: k). TyCon a -> TTypeRep a
pattern type TRApp :: forall k. exists k1 (a :: k1 -> k) (b :: k1).
TTypeRep a -> TTypeRep b -> TTypeRep (a b)
pattern type TRFun :: TTypeRep arg
-> TTypeRep res
-> TypeRep (TTypeRep (arg->res))
-- For now, homogeneous equalities
eqTyCon :: forall k (a :: k) (b :: k).
TTyCon a -> TTyCon b -> Maybe (a :~: b)
eqTT :: forall k (a :: k) (b :: k).
TTypeRep a ->T TypeRep b -> Maybe (a :~: b)
```
dataTTypeRep(a :: k)-- abstractdataTTyCon(a :: k)-- abstract-- CostructorstrCon:: forall k (a :: k).TTyCon a ->TTypeRep a -- in TCBtrApp:: forall k k1 (a :: k1 -> k)(b :: k1).TTypeRep a ->TTypeRep b ->TTypeRep(a b)-- in TCB-- DestructorspatterntypeTRCon:: forall k (a :: k).TyCon a ->TTypeRep a
patterntypeTRApp:: forall k. exists k1 (a :: k1 -> k)(b :: k1).TTypeRep a ->TTypeRep b ->TTypeRep(a b)patterntypeTRFun::TTypeRep arg
->TTypeRep res
->TypeRep(TTypeRep(arg->res))-- For now, homogeneous equalitieseqTyCon:: forall k (a :: k)(b :: k).TTyCon a ->TTyCon b ->Maybe(a :~: b)eqTT:: forall k (a :: k)(b :: k).TTypeRep a ->TTypeRep b ->Maybe(a :~: b)
```
This assumes heterogeneous equality (that is, with kind equalities).
```wiki
data TTypeRep (a :: k) -- abstract
data TTyCon (a :: k) -- abstract
tyConKind :: forall k (a :: k). TTyCon a -> TTypeRep k
-- Costructors
trCon :: forall k (a :: k). TTyCon a -> TTypeRep a
trApp :: forall k k1 (a :: k1 -> k) (b :: k1).
TTypeRep a -> TTypeRep b -> TTypeRep (a b)
-- Destructors
pattern type TRCon :: forall k (a :: k). TyCon a -> TTypeRep a
pattern type TRApp :: forall k. exists k1 (a :: k1 -> k) (b :: k1).
TTypeRep a -> TTypeRep b -> TTypeRep (a b)
-- this definition to go into Data.Type.Equality
data (a :: k1) :~~: (b :: k2) where
HRefl :: a :~~: a
eqTyCon :: forall k1 k2 (a :: k1) (b :: k2).
TTyCon a -> TTyCon b -> Maybe (a :~~: b)
-- the following definitions can be defined on top of the interface
-- above, but would be included for convenience
pattern type TRFun :: TTypeRep arg -> TTypeRep res
-> TTypeRep (arg -> res)
```
dataTTypeRep(a :: k)-- abstractdataTTyCon(a :: k)-- abstracttyConKind:: forall k (a :: k).TTyCon a ->TTypeRep k
eqTT :: forall k1 k2 (a :: k1) (b :: k2).
TTypeRep a -> TTypeRep b -> Maybe (a :~~: b)
-- CostructorstrCon:: forall k (a :: k).TTyCon a ->TTypeRep a
trApp:: forall k k1 (a :: k1 -> k)(b :: k1).TTypeRep a ->TTypeRep b ->TTypeRep(a b)-- DestructorspatterntypeTRCon:: forall k (a :: k).TyCon a ->TTypeRep a
patterntypeTRApp:: forall k. exists k1 (a :: k1 -> k)(b :: k1).TTypeRep a ->TTypeRep b ->TTypeRep(a b)-- this definition to go into Data.Type.Equalitydata(a :: k1):~~:(b :: k2)whereHRefl:: a :~~: a
typeRepKind :: forall k (a :: k). TTypeRep a -> TTypeRep k
eqTyCon:: forall k1 k2 (a :: k1)(b :: k2).TTyCon a ->TTyCon b ->Maybe(a :~~: b)-- the following definitions can be defined on top of the interface-- above, but would be included for conveniencepatterntypeTRFun::TTypeRep arg ->TTypeRep res
->TTypeRep(arg -> res)eqTT:: forall k1 k2 (a :: k1)(b :: k2).TTypeRep a ->TTypeRep b ->Maybe(a :~~: b)typeRepKind:: forall k (a :: k).TTypeRep a ->TTypeRep k
class forall k (a :: k). Typeable k => Typeable a where
tTypeRep :: TTypeRep a
class forall k (a :: k).Typeable k =>Typeable a where
tTypeRep ::TTypeRep a
```
**SLPJ**: Do we need both `:~:` and `:~~:`?
......@@ -452,30 +361,30 @@ As painfully demonstrated (painful in the conclusion, not the demonstration!) in
Drawing this out somewhat: we allow only `Typeable` instances for unapplied constructors. That is, we have
```wiki
deriving instance Typeable Maybe
```
derivinginstanceTypeableMaybe
```
never
```wiki
deriving instance Typeable (Maybe Int)
```
derivinginstanceTypeable(MaybeInt)
```
However, what if we have
```wiki
data PK (a :: k)
```
dataPK(a :: k)
```
? `PK` properly has *two* parameters: the kind `k` and the type `a :: k`. However, whenever we write `PK` in source code, the `k` parameter is implicitly provided. Thus,
when we write
```wiki
deriving instance Typeable PK
```
derivinginstanceTypeablePK
```
......@@ -493,9 +402,8 @@ The "obvious" answer -- don't supply the `k` here -- doesn't work. The instance
One (somewhat unpleasant) way forward is to allow kind parameters to be supplied in `Typeable` instances, but still restrict type parameters. So, we would have
```wiki
deriving instance Typeable (PK :: * -> *)
deriving instance Typeable (PK :: (* -> *) -> *)
```
derivinginstanceTypeable(PK::*->*)derivinginstanceTypeable(PK::(*->*)->*)
```
......@@ -529,27 +437,23 @@ Some drawbacks:
We actually don't have a good long-term solution available. We thought that `* :: *` and kind equalities would fix this, but they don't. To see why, let's examine the type of `trApp`:
```wiki
trApp :: forall k k1 (a :: k1 -> k) (b :: k1).
TTypeRep a -> TTypeRep b -> TTypeRep (a b)
```
trApp:: forall k k1 (a :: k1 -> k)(b :: k1).TTypeRep a ->TTypeRep b ->TTypeRep(a b)
```
In the `* :: *` world, it would be reasonable to have `TTypeRep`s for kinds, assuming we have `TTypeRep`s always take explicit kind parameters. So, we might imagine having a `TTypeRep` for `PK` (call it `pkRep`) and a `TTypeRep` for `Bool` (call it `boolRep`). Does `pkRep `trApp` boolRep`` type-check? Unfortunately, no. We have
```wiki
pkRep :: TTypeRep <forall k. k -> *> PK
boolRep :: TTypeRep <*> Bool
```
pkRep::TTypeRep<forall k. k ->*>PKboolRep::TTypeRep<*>Bool
```
but `trApp` says that `a` must have type `k1 -> k` for some `k1` and `k`. Here `PK` would be the value for `a`, but `PK`'s kind is `forall k. k -> *`, which doesn't fit `k1 -> k` at all! We would need to generalize `trApp` to
```wiki
trApp2 :: forall (k1 :: *) (k :: k1 -> *)
(a :: pi (b :: k1). k b) (b :: k1).
TTypeRep <pi (b :: k1). k b> a -> TTypeRep <k1> b
-> TTypeRep <k b> (a b)
```
trApp2:: forall (k1 ::*)(k :: k1 ->*)(a :: pi (b :: k1). k b)(b :: k1).TTypeRep<pi (b :: k1). k b> a ->TTypeRep<k1> b
->TTypeRep<k b>(a b)
```
......