... | ... | @@ -9,189 +9,294 @@ The names of functions and type constructors is totally up for grabs. |
|
|
## Goal
|
|
|
|
|
|
|
|
|
Our goal is some polykinded type
|
|
|
Consider `Dynamic`:
|
|
|
|
|
|
```wiki
|
|
|
TypeRep a
|
|
|
data Dynamic where
|
|
|
Dyn :: TypeRep -> a -> Dynamic
|
|
|
```
|
|
|
|
|
|
|
|
|
so that casting is safe
|
|
|
We'd like to write `dynApply`:
|
|
|
|
|
|
```wiki
|
|
|
gcast :: forall k. forall (a :: k). forall (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b)
|
|
|
dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
|
|
|
```
|
|
|
|
|
|
|
|
|
and that is also safely decomposable, i.e. we need some analogue of
|
|
|
which succeeds only when the application is type correct. But how? Let's try
|
|
|
|
|
|
```wiki
|
|
|
splitTyConApp :: TypeRep -> (TyCon, [TypeRep])
|
|
|
dynApply (Dyn tf f) (Dyn tx x) = ???
|
|
|
```
|
|
|
|
|
|
|
|
|
for `TypeRep a` so that we can figure out whether a given type is an arrow type, product type, etc.
|
|
|
We need some way to decompose `tf` (the type representation for `f`), ask if it is an arrow type, and if so extract the type representation for the argument and result type. Then we need to compare the argument type with `xt`'s representation. If so, we are good to go.
|
|
|
|
|
|
|
|
|
This capability is necessary to implement `dynApply` for Typeable based dynamic typing, without making `dynApply` part of the Trusted Code Base. So `dynApply` makes a "poster-child" example.
|
|
|
But at the moment we don't have any *type-safe* way to decompose `TypeRep`. Indeed `dynApply` is defined like this right now:
|
|
|
|
|
|
```wiki
|
|
|
data Dynamic where
|
|
|
Dyn :: Typeable a => a -> Dynamic
|
|
|
|
|
|
dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
|
|
|
dynApply (Dyn tf f) (Dyn tx x)
|
|
|
= case funResultTy tf tx of
|
|
|
Just tr -> Just (Dyn tr (unsafeCoerce f x))
|
|
|
```
|
|
|
|
|
|
### Typeable a vs TypeRep a
|
|
|
|
|
|
where `funResultTy :: TypeRep -> TypeRep -> Maybe TypeRep` does the decomposition of `tf`, checking that it is of form `tx -> tr`.
|
|
|
|
|
|
|
|
|
The `unsafeCoerce` makes `dynApply` part of the Trusted Code Base (TCB). That might not be so bad, but it is a poster-child for a raft of other similar functions (e.g. in Cloud Haskell).
|
|
|
|
|
|
|
|
|
So **our main goal is to be able to write `dynApply` in a type-safe way** so that it is not part of the TCB.
|
|
|
|
|
|
---
|
|
|
|
|
|
## Step 1: Type-indexed type representations
|
|
|
|
|
|
|
|
|
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
|
|
|
```
|
|
|
|
|
|
|
|
|
Currently `Typaeble a` is a type class, indexed by the type `a`; while `TypeRep` is a data type, with no type index (i.e. it has arity zero). But it's often useful to be able pass a type-indexed value around directly, rather than indirectly as a type class. It often makes the code clearer, especially in tricky cases, and much less laden with `proxy` arguments.
|
|
|
Here we are using a *type-indexed* type representation, `TTypeRep`. Now the connection betweeen the two is visible to the type system.
|
|
|
|
|
|
|
|
|
So in this page we explore the possibility of making `TypeRep` type-indexed too, like this:
|
|
|
We can re-define the `Typeable` class and `TypeRep` thus:
|
|
|
|
|
|
```wiki
|
|
|
class Typeable a where
|
|
|
typeRep :: TypeRep a
|
|
|
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)
|
|
|
```
|
|
|
|
|
|
|
|
|
We'll need to add the following primitive to make sure that we always
|
|
|
have access to the Typeable class, even if we produce the TypeRep by pattern matching.
|
|
|
It is helpful to have both `Typeable a` (the class) and `TTypeRep a` (the value).
|
|
|
|
|
|
- It is sometimes convenient to pass a `TTypeRep` around implicitly (via a `Typeable a =>` constraint).
|
|
|
- But in tricky cases, it is also often much clearer (and less laden with proxy arguments) to pass it around as an ordinary, named 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 :: TypeRep a -> (Typeable a => b) -> b
|
|
|
withTypeable :: TTypeRep a -> (Typeable a => b) -> b
|
|
|
```
|
|
|
|
|
|
|
|
|
(This seems both simpler and more useful than making the Typeable class recursive through TypeRep data declaration.)
|
|
|
|
|
|
|
|
|
Now we can define `Dynamic` either as above or, equivalently and more concretely, thus:
|
|
|
We can also compare two `TTypeReps` to give a statically-usable proof of equality:
|
|
|
|
|
|
```wiki
|
|
|
data Dynamic where
|
|
|
Dyn :: TypeRep a -> a -> Dynamic
|
|
|
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
|
|
|
```
|
|
|
|
|
|
|
|
|
This change is somewhat orthogonal to the question of making a strongly-typed `DynApply`.
|
|
|
(`eqT` and `:~:` exist already as part of the exports of `Data.Typeable`.)
|
|
|
|
|
|
### Kind equalities are sufficient
|
|
|
---
|
|
|
|
|
|
## Step 2: Decomposing functions
|
|
|
|
|
|
Here is the natural GADT to use for `TypeRep`:
|
|
|
|
|
|
If we want to decompose `TTypable`, at least in the function arrow case, we need a function like this:
|
|
|
|
|
|
```wiki
|
|
|
{-# LANGUAGE PolyKinds, DataKinds, EmptyDataDecls, GADTs #-}
|
|
|
data TypeRep (a :: k) :: * where
|
|
|
TRApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
|
|
|
TRCon :: TyCon a -> TypeRep a
|
|
|
decomposeFun :: TTypeRep fun
|
|
|
-> r
|
|
|
-> (forall arg res. (fun ~ (arg->res))
|
|
|
=> TypeRep 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'
|
|
|
```
|
|
|
|
|
|
|
|
|
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 quesiton.)
|
|
|
This function is part of `Typeable`, and replaces `funResultTy`.
|
|
|
|
|
|
|
|
|
Pattern matching TypeRep would produce a TyCon with unknown kind but any cast function we could write, i.e.
|
|
|
Now we can write `dynApply`, in a completely type-safe way, outside the TCB:
|
|
|
|
|
|
```wiki
|
|
|
eqTyCon :: forall (a b :: k). TyCon a -> TyCon b -> Maybe (a :~: b)
|
|
|
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 -> 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:
|
|
|
|
|
|
must require the two arguments to have the same kind.
|
|
|
```wiki
|
|
|
pattern type TRFun :: TTypeRep arg
|
|
|
-> TTypeRep res
|
|
|
-> TypeRep (TTypeRep (arg->res))
|
|
|
```
|
|
|
|
|
|
|
|
|
If we have kind equalities available, we could produce evidence that the kinds are equal too. We need a kind-indexed GADT to package that evidence up in a heterogenous equality type.
|
|
|
which looks (by design) very like the signature for a GADT data constructor. Now we can use `TRFun` in a pattern, thus:
|
|
|
|
|
|
```wiki
|
|
|
data JMeq (a :: k1) (b :: k2) where
|
|
|
JMRefl :: JMeq a a
|
|
|
dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
|
|
|
dynApply (Dyn (TRFun ta tr) f) (Dyn tx x)
|
|
|
= case eqTT ta tx of
|
|
|
Nothing -> Nothing
|
|
|
Just Refl -> Dyn tr (f x)
|
|
|
dynApply _ _ = Nothing
|
|
|
```
|
|
|
|
|
|
|
|
|
With this GADT, we can generalize the type of eqTyCon
|
|
|
Is that not beautiful? The second equation for `dynApply` is needed in case the `TRFun` pattern does not match.
|
|
|
|
|
|
---
|
|
|
|
|
|
## Step 3: Decomposing arbitrary types
|
|
|
|
|
|
|
|
|
It is all very well being able to decompose functions, but what about decomposing other types, like `Maybe Int`?
|
|
|
|
|
|
|
|
|
To do this it is natural to regard types as built from type constructors and binary application, like this:
|
|
|
|
|
|
```wiki
|
|
|
eqTyCon :: forall (k1 k2 :: *). forall (a :: k1). forall (b :: k2). TyCon a -> TyCon b -> Maybe (JMeq a b)
|
|
|
data TTypeRep (a :: k) :: * where
|
|
|
TRApp :: 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 -> *
|
|
|
```
|
|
|
|
|
|
|
|
|
For example, imagine if we had this representation available
|
|
|
(We could, and ultimately should, use pattern synonyms again, but it's more concrete to use a GADT for now. Perhaps surprisingly, it is actually fine to expose `TTypeRep` concretely, with its constructors; we can't construct ill-formed `TTypeRep`s.)
|
|
|
|
|
|
|
|
|
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
|
|
|
arrowCon :: TyCon (->)
|
|
|
TRApp :: forall k1 k2. forall (a :: k1 -> k2) (b :: k1).
|
|
|
TTypeRep <k1->k2> a -> TTypeRep <k2> b -> TTypeRep <k2> (a b)
|
|
|
```
|
|
|
|
|
|
|
|
|
and wanted to implement the following function:
|
|
|
Or, to be really explicit about the existentials:
|
|
|
|
|
|
```wiki
|
|
|
ifArrow :: forall (a d :: *). TypeRep a -> (forall b c . TypeRep b -> TypeRep c -> d) -> d -> d
|
|
|
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
|
|
|
```
|
|
|
|
|
|
|
|
|
This implementation could be:
|
|
|
Now suppose we want to implement `decomposeFun`. We should be able to do this outside the TCB, i.e. without `unsafeCoerce`:
|
|
|
|
|
|
```wiki
|
|
|
ifArrow tr f default = case tr of
|
|
|
TRApp (TRApp c r1) r2 -> case eqTyCon c arrowCon of
|
|
|
Just JMRefl -> f r1 r2
|
|
|
Nothing -> default
|
|
|
_ -> default
|
|
|
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
|
|
|
```
|
|
|
|
|
|
|
|
|
Note that with the first version of `eqTyCon` this code would not type check.
|
|
|
But look at the arguments of `eqTyCon`:
|
|
|
|
|
|
```wiki
|
|
|
arrowCon :: TTyCon <*->*->*> (->)
|
|
|
c :: TTyCon <k1->k2->*> tc
|
|
|
```
|
|
|
|
|
|
|
|
|
This interface of `ifArrow` is just what we need for `dynApply`.
|
|
|
where `k1` and `k2` are existential kinds bound by the two nested `TRApp` constructors, and `tc` the existential bound by the inner `TRApp`. But `kont` is expecting `arg` and `res` to have kind `*`! So we need proofs that `k1 ~ *` and `k2 ~ *`.
|
|
|
|
|
|
|
|
|
The real work is done by `eqTyCon`:
|
|
|
|
|
|
```wiki
|
|
|
dynApply :: Dynamic -> Dynamic -> Dynamic
|
|
|
dynApply (Dyn a) (Dyn (b :: b)) =
|
|
|
ifArrow a (\ dom rng -> gcast dom (typeRep :: TypeRep b) of
|
|
|
Just Refl -> Dyn (a b)
|
|
|
Nothing -> default) default where default = Dyn (error "can't apply")
|
|
|
eqTyCon :: forall (k1 k2 :: *).
|
|
|
forall (a :: k1) (b :: k2).
|
|
|
TTyCon <k1> a -> TTyCon <k2> b -> Maybe (a :~~: b)
|
|
|
```
|
|
|
|
|
|
|
|
|
Alternatively, we could give a different interface for decomposing arrow types with the addition of a new data structure.
|
|
|
where `:~~:` is a *kind-heterogeneous* version of `:~:`:
|
|
|
|
|
|
```wiki
|
|
|
data ArrowTy where
|
|
|
Arrow :: forall (a b :: *). TypeRep a -> TypeRep b -> ArrowTy
|
|
|
data (a::k1) :~~: (b::k2) where
|
|
|
HRefl :: forall (a::k). a :~~: a
|
|
|
```
|
|
|
|
|
|
|
|
|
ifArrow :: TypeRep a -> Maybe ArrowTy
|
|
|
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
|
|
|
```
|
|
|
|
|
|
### Fast comparison of `TypeRep`
|
|
|
|
|
|
That is, `HRefl` encapsulates a proof of kind equality as well as one of type equality.
|
|
|
|
|
|
The current implementation of `TypeRep` allows constant-type comparison based on fingerprints. To support this in the new scheme we would want to add a fingerprint to every `TypeRep` node. But we would not want clients to see those fingerprints, lest they forge them.
|
|
|
|
|
|
So Step 3 (allowing `TypeRep` to be fully decomposed in a type safe way) absolutely requires kind equalities.
|
|
|
|
|
|
Conclusion: make `TypeRep` abstract. But then how can we pattern-match on it? Pattern synonyms seem to be exactly what we need.
|
|
|
---
|
|
|
|
|
|
### What can we do without kind equalities ?
|
|
|
## Other points
|
|
|
|
|
|
### Fast comparison of `TypeRep`
|
|
|
|
|
|
|
|
|
The current implementation of `TypeRep` allows constant-type comparison based on fingerprints. To support this in the new scheme we would want to add a fingerprint to every `TypeRep` node. But we would not want clients to see those fingerprints, lest they forge them.
|
|
|
|
|
|
Before kind equalities are available, we can still offer decomposition, by making `ifArrow` and other destructors primitive; i.e. part of the TCB.
|
|
|
|
|
|
Conclusion: make `TypeRep` abstract. But then how can we pattern-match on it? Pattern synonyms seem to be exactly what we need.
|
|
|
|
|
|
### Trusted computing base
|
|
|
|
|
|
|
|
|
The `TyCon` type is a new abstract type, and the comparison (based on fingerprints) must be in the TCB.
|
|
|
With all of this, what is left in the TCB? The `TyCon` type is a new abstract type, and the comparison (based on fingerprints) must be in the TCB.
|
|
|
|
|
|
```wiki
|
|
|
TyCon a --- abstract type
|
|
|
eqTyCon :: forall (k1 k2 :: *). forall (a :: k1). forall (b :: k2). TyCon a -> TyCon b -> Maybe (JMeq a b)
|
|
|
TTyCon a --- abstract type
|
|
|
eqTyCon :: forall k1 k2. forall (a :: k1) (b :: k2).
|
|
|
TTyCon a -> TTyCon b -> Maybe (a :~~: b)
|
|
|
```
|
|
|
|
|
|
|
|
|
This could be written in core (and perhaps could be generalized to other constraints) but not in source Haskell:
|
|
|
`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
|
... | ... | @@ -202,33 +307,55 @@ withTypeable :: TypeRep a -> (Typeable a => b) -> b |
|
|
|
|
|
Related but different issue: [ https://ghc.haskell.org/trac/ghc/ticket/7897](https://ghc.haskell.org/trac/ghc/ticket/7897)
|
|
|
|
|
|
## Proposed API
|
|
|
---
|
|
|
|
|
|
## Step by step
|
|
|
|
|
|
```wiki
|
|
|
data TypeRep (a :: k) -- abstract
|
|
|
data TyCon (a :: k) -- abstract
|
|
|
|
|
|
pattern TyCon :: forall k (a :: k). TyCon a -> TypeRep a
|
|
|
pattern TyApp :: forall k. exists k1 (a :: k1 -> k) (b :: k1). TypeRep a -> TypeRep b -> TypeRep (a b)
|
|
|
We can do steps 1 and 2 without kind equalities, although the
|
|
|
implementation of `decomposeFun` will use `unsafeCoerce` and will be part of the TCB.
|
|
|
|
|
|
## Proposed API
|
|
|
|
|
|
tyCon :: forall k (a :: k). TyCon a -> TypeRep a -- in TCB
|
|
|
apply :: forall k k1 (a :: k1 -> k) (b :: k1). TypeRep a -> TypeRep b -> TypeRep (a b) -- in TCB
|
|
|
```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)
|
|
|
```
|
|
|
|
|
|
-- data (a :: k1) :~~: (b :: k2) where
|
|
|
-- HRefl :: a :~~: a
|
|
|
|
|
|
-- eqTyCon :: forall k1 k2 (a :: k1) (b :: k2). TyCon a -> TyCon b -> Maybe (a :~~: b)
|
|
|
-- eqT :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~~: b)
|
|
|
When we get kind equalities, we can generalise `eqTyCon` and `eqTT`:
|
|
|
|
|
|
eqTyCon :: forall k (a :: k) (b :: k). TyCon a -> TyCon b -> Maybe (a :~: b)
|
|
|
eqT :: forall k (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b)
|
|
|
```wiki
|
|
|
data (a :: k1) :~~: (b :: k2) where
|
|
|
HRefl :: a :~~: a
|
|
|
|
|
|
ifArrow :: forall (a :: *) (d :: *). TypeRep a -> (forall (b :: *) (c :: *).
|
|
|
TypeRep b -> TypeRep c -> (a :~: (b -> c)) -> d) -> d
|
|
|
eqTyCon :: forall k1 k2 (a :: k1) (b :: k2).
|
|
|
TTyCon a -> TTyCon b -> Maybe (a :~~: b)
|
|
|
eqT :: forall k1 k2 (a :: k1) (b :: k2).
|
|
|
TTypeRep a -> TTypeRep b -> Maybe (a :~~: b)
|
|
|
```
|
|
|
|
|
|
|
|
|
The commented out bit in the middle is what would be used if we had kind equalities. Sadly, we don't yet.
|
|
|
**SLPJ**: Do we need both `:~:` and `:~~:`?
|
|
|
|
|
|
|
|
|
Some of this design is motivated by the desire to allow flexibility in the implementation to allow for fingerprinting for fast equality comparisons. Naturally, the fingerprints have to be in the TCB. If it weren't for them, though, the `TypeRep` type could be exported concretely.
|
... | ... | |