Type-indexed Typeable

[bgamari]

Here is a proposal for augmenting our existing Typeable mechanism with a variant, Type.Reflection, which provides a more strongly typed variant as originally described in A Reflection on Types (Peyton Jones, et al. 2016).

Rendered

[RyanGlScott]

This implementation of dynApply doesn't seem right, especially since it uses unsafeCoerce. Perhaps this definition was copy-pasted from above and wasn't updated? For reference, the definition in your branch is:

dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
dynApply (Dynamic (TRFun ta tr) f) (Dynamic ta' x)
  | Just HRefl <- ta `eqTypeRep` ta'              = Just (Dynamic tr (f x))
dynApply _ _ = Nothing

[bgamari]

Oh no! Indeed, copy/paste error. Thanks for pointing this out!

[goldfirere]

A few points as I drove by:

• This proposal depends on a definition for :~~:, which I believe is absent.
• someTypeRep does not look all that useful (the one that takes a proxy). Remove?
• Should the TyCon constructor take the kind parameters used to instantiate kind-polymorphic tycons?
• Will TypeRep be concrete? It's unclear from this proposal. I vote "no".

Thanks thanks thanks!

[goldfirere]

A few points as I drove by:

• This proposal depends on a definition for :~~:, which I believe is absent.
• someTypeRep does not look all that useful (the one that takes a proxy). Remove?
• Should the TyCon constructor take the kind parameters used to instantiate kind-polymorphic tycons?
• Will TypeRep be concrete? It's unclear from this proposal. I vote "no".

Thanks thanks thanks!

[bgamari]

A few points as I drove by:

Thanks!

This proposal depends on a definition for :~~:, which I believe is absent.

Good catch.

someTypeRep does not look all that useful (the one that takes a proxy). Remove?

Indeed it. I don't remember why I originally introduced it but I agree, it doesn't seem to serve a purpose.

Should the TyCon constructor take the kind parameters used to instantiate kind-polymorphic tycons?

This is a rather tricky trade-off.
Under a type-indexed TyCon scheme, the compiler would need to emit a polymorphic function binding for every time declaration. For instance, in the case of,

data Proxy (a :: k) :: Type

we would need to emit,

proxyTyCon :: TypeRep k -> TyCon (Proxy (a :: k))

And then producing evidence for, e.g., typeRep @(Proxy Int) we would emit,

TRApp (TRCon (proxyTyCon (typeRep @Type))) (typeRep @Int)

By contrast under the current non-indexed scheme we would emit,

TRApp (TRCon proxyTyCon) (typeRep @Int)

In effect this has turned what is a static data reference under the current, non-indexed scheme into a polymorphic function call. I worry what effect this would have on both compile- and run-time as we currently try quite hard to use efficient encodings for TyCon

I was proposing that we keep this pattern unidirectional for this very reason (which the proposal really ought to make more clear).

I really don't think we lose much power under the proposed non-indexed scheme; the only thing we cannot do its instantiate a TRCon at a new kind (which we couldn't do with perfect reliability with an indexed TyCon due to the imprecision of UnboxedTupleRep).

Will TypeRep be concrete? It's unclear from this proposal. I vote "no".

I agree except for limited exposure via pattern synonyms and perhaps through an internal module (e.g. Data.Typeable.Internal)..

Thanks thanks thanks!

Thanks!

[bgamari]

A few points as I drove by:

Thanks!

This proposal depends on a definition for :~~:, which I believe is absent.

Good catch.

someTypeRep does not look all that useful (the one that takes a proxy). Remove?

Indeed it. I don't remember why I originally introduced it but I agree, it doesn't seem to serve a purpose.

Should the TyCon constructor take the kind parameters used to instantiate kind-polymorphic tycons?

This is a rather tricky trade-off.
Under a type-indexed TyCon scheme, the compiler would need to emit a polymorphic function binding for every time declaration. For instance, in the case of,

data Proxy (a :: k) :: Type

we would need to emit,

proxyTyCon :: TypeRep k -> TyCon (Proxy (a :: k))

And then producing evidence for, e.g., typeRep @(Proxy Int) we would emit,

TRApp (TRCon (proxyTyCon (typeRep @Type))) (typeRep @Int)

By contrast under the current non-indexed scheme we would emit,

TRApp (TRCon proxyTyCon) (typeRep @Int)

In effect this has turned what is a static data reference under the current, non-indexed scheme into a polymorphic function call. I worry what effect this would have on both compile- and run-time as we currently try quite hard to use efficient encodings for TyCon

I was proposing that we keep this pattern unidirectional for this very reason (which the proposal really ought to make more clear).

I really don't think we lose much power under the proposed non-indexed scheme; the only thing we cannot do its instantiate a TRCon at a new kind (which we couldn't do with perfect reliability with an indexed TyCon due to the imprecision of UnboxedTupleRep).

Will TypeRep be concrete? It's unclear from this proposal. I vote "no".

I agree except for limited exposure via pattern synonyms and perhaps through an internal module (e.g. Data.Typeable.Internal)..

Thanks thanks thanks!

Thanks!

[goldfirere]

You make some compelling arguments about indexing TyCon (or, rather, not indexing it). I was thrown off by your explicit comment saying that TRCon is bidirectional, which is why I then assumed to meant to index TyCon all along.

Of course, I'm +1 on this direction, but it's hard to give a final stamp of approval without the full API written out. But perhaps it's too early to insist on a full API.

[goldfirere]

You make some compelling arguments about indexing TyCon (or, rather, not indexing it). I was thrown off by your explicit comment saying that TRCon is bidirectional, which is why I then assumed to meant to index TyCon all along.

Of course, I'm +1 on this direction, but it's hard to give a final stamp of approval without the full API written out. But perhaps it's too early to insist on a full API.

[AshleyYakeley]

Nice. Consider adding a heterogenous version of class TestEquality to go with your :~~:.

[Icelandjack]

See @goldfirere's comment

[AshleyYakeley]

A more general "Some" class might be more useful? data Some f = forall a. Some (f a)

[adamgundry]

It might indeed.

That said, now that we have TypeInType, would it be that crazy to rename SomeTypeRep to Type (or * in old fashioned language)? At the term level, we should just be able to write functions that manipulate runtime representations of types! (Here's a half-baked exploration of this idea using the existing (GHC 8.0.1) Typeable.)

[goldfirere]

Well, this new indexed TypeRep is just the singleton associated with Type. But until we can do this right, I wouldn't want to make forward-compatibility troubles by naming this existential Type, even though it is indeed isomorphic to Type.

[dcoutts]

As someone interested in serialising these things (e.g. for Cloud Haskell), I don't mind how it's done too much provided that it is still quick! Doesn't matter too much if it's more complicated or not backwards compatible.

[dcoutts]

As someone interested in serialising these things (e.g. for Cloud Haskell), I don't mind how it's done too much provided that it is still quick! Doesn't matter too much if it's more complicated or not backwards compatible.

[bgamari]

@dcoutts indeed the cost associated with serialization of the full TypeRep is potential a sticky point (although no worse than the current scheme). However, you can always just serialize the fingerprint (which IIRC is precisely what Cloud Haskell does).

[bgamari]

@dcoutts indeed the cost associated with serialization of the full TypeRep is potential a sticky point (although no worse than the current scheme). However, you can always just serialize the fingerprint (which IIRC is precisely what Cloud Haskell does).

[Icelandjack]

For Data.Dynamic I would like to see SDynamic:

data SDynamic s where
  SDynamic :: TypeRep a -> s a -> SDynamic s

(see Value)

[Icelandjack]

For Data.Dynamic I would like to see SDynamic:

data SDynamic s where
  SDynamic :: TypeRep a -> s a -> SDynamic s

(see Value)

[bgamari]

Icelandjack notifications@github.com writes:

For Data.Dynamic I would like to see SDynamic:

data SDynamic s where
  SDynamic :: TypeRep a -> s a -> SDynamic s

Alright, I don't see any reason why we couldn't provide this. That being
said, I'm not a fan of the name; why S?

[bgamari]

Icelandjack notifications@github.com writes:

For Data.Dynamic I would like to see SDynamic:

data SDynamic s where
  SDynamic :: TypeRep a -> s a -> SDynamic s

Alright, I don't see any reason why we couldn't provide this. That being
said, I'm not a fan of the name; why S?

[goldfirere]

While this SDynamic might be useful, I'm not sure why this construction, specially, should appear in Data.Dynamic. There are a good many (infinite number?) similar constructs that we might include. Why is this one better than all its siblings?

And, of course, a separate library could provide this functionality. Indeed, Data.Dynamic need not be in base at all. (Perhaps it really shouldn't be.)

[goldfirere]

While this SDynamic might be useful, I'm not sure why this construction, specially, should appear in Data.Dynamic. There are a good many (infinite number?) similar constructs that we might include. Why is this one better than all its siblings?

And, of course, a separate library could provide this functionality. Indeed, Data.Dynamic need not be in base at all. (Perhaps it really shouldn't be.)

[Icelandjack]

@bgamari: Probably Shape or Static based on

SDynamic is a mid-point between fully dynamic & fully static types. We statically know some "Shape" information, but not all info about type. e.g., SDynamic Maybe contains a value that is definitely a Maybe ty for some type ty, but the type ty can vary between values of type SDynamic Maybe.

I don't care for the name particularly.

We could look to ... for functions to include, some like value :: Value f -> f Any won't make sense given the different representation (type-indexed type representation vs Any).

data Wrapper a = Wrapper
  (forall g. g a -> SDynamic g)
  (forall g. SDynamic g -> g a)

-- Unwrap a value to get at the thing inside, while still being able
-- to wrap it up again.
data Unwrapped f where
  In :: f a -> Wrapper a -> Unwrapped f

mapSDynamic :: (f ~> g) -> (SDynamic f -> SDynamic g)
ofSDynamic  :: (forall a. f a -> b) -> (SDynamic f -> b)
...

@goldfirere That would be fine too, do you think discussions pertaining to Dynamic should be moved elsewhere? We could look to mirror the gcast family of functions (I haven't played with these at all)

gcast  :: (Typeable a, Typeable b)  => s a       -> Maybe (s b)
gcast1 :: (Typeable t, Typeable t') => s (t a)   -> Maybe (s (t' a))
gcast2 :: (Typeable t, Typeable t') => s (t a b) -> Maybe (s (t' a b))

-- ???????
data SDynamic  s     where SDynamic  :: TypeRep a -> s a       -> SDynamic  s
data SDynamic1 s a   where SDynamic1 :: TypeRep t -> s (t a)   -> SDynamic1 s a
data SDynamic2 s a b where SDynamic2 :: TypeRep t -> s (t a b) -> SDynamic2 s a b

constraints chose the following quantified constraints forall a. p a, forall a. p (f a) and forall f a. p (t f a).

[Icelandjack]

@bgamari: Probably Shape or Static based on

SDynamic is a mid-point between fully dynamic & fully static types. We statically know some "Shape" information, but not all info about type. e.g., SDynamic Maybe contains a value that is definitely a Maybe ty for some type ty, but the type ty can vary between values of type SDynamic Maybe.

I don't care for the name particularly.

We could look to ... for functions to include, some like value :: Value f -> f Any won't make sense given the different representation (type-indexed type representation vs Any).

data Wrapper a = Wrapper
  (forall g. g a -> SDynamic g)
  (forall g. SDynamic g -> g a)

-- Unwrap a value to get at the thing inside, while still being able
-- to wrap it up again.
data Unwrapped f where
  In :: f a -> Wrapper a -> Unwrapped f

mapSDynamic :: (f ~> g) -> (SDynamic f -> SDynamic g)
ofSDynamic  :: (forall a. f a -> b) -> (SDynamic f -> b)
...

@goldfirere That would be fine too, do you think discussions pertaining to Dynamic should be moved elsewhere? We could look to mirror the gcast family of functions (I haven't played with these at all)

gcast  :: (Typeable a, Typeable b)  => s a       -> Maybe (s b)
gcast1 :: (Typeable t, Typeable t') => s (t a)   -> Maybe (s (t' a))
gcast2 :: (Typeable t, Typeable t') => s (t a b) -> Maybe (s (t' a b))

-- ???????
data SDynamic  s     where SDynamic  :: TypeRep a -> s a       -> SDynamic  s
data SDynamic1 s a   where SDynamic1 :: TypeRep t -> s (t a)   -> SDynamic1 s a
data SDynamic2 s a b where SDynamic2 :: TypeRep t -> s (t a b) -> SDynamic2 s a b

constraints chose the following quantified constraints forall a. p a, forall a. p (f a) and forall f a. p (t f a).

[goldfirere]

I believe (and IIRC, my opinion is shared somewhat widely) that base should be as small as possible. Dynamic and friends are a feature relatively few people need. In its current form, the safety of the Dynamic construction is not specified by the Report (I think), and therefore it is appropriate that the implementation be blessed by putting it in base. With the new TypeRep, this is no longer the case, as Dynamic can be built on TypeRep without any special considerations.

I do think we should make sure that a solid implementation of Dynamic can be built on our new design of TypeRep, as a check on our design. But we don't have to actually package that implementation.

[goldfirere]

I believe (and IIRC, my opinion is shared somewhat widely) that base should be as small as possible. Dynamic and friends are a feature relatively few people need. In its current form, the safety of the Dynamic construction is not specified by the Report (I think), and therefore it is appropriate that the implementation be blessed by putting it in base. With the new TypeRep, this is no longer the case, as Dynamic can be built on TypeRep without any special considerations.

I do think we should make sure that a solid implementation of Dynamic can be built on our new design of TypeRep, as a check on our design. But we don't have to actually package that implementation.

[Icelandjack]

dynHead :: Dynamic -> Maybe Dynamic
dynHead (Dyn (rxs :: TypeRep txs) (xs :: txs)) = do
  App rl rx <- splitApp rxs
  Refl <- rl `eqT` (typeRep :: TypeRep [])
  return (Dyn rx (head xs))

can look nicer

pattern (:<->:) :: () => fa ~ f a => TypeRep f -> TypeRep a -> TypeRep fa
pattern f :<->: a <- (splitApp -> Just (App f a))
  where f :<->: a = TypeApp f a

dynHead :: Dynamic -> Maybe Dynamic
dynHead (Dyn (f :<->: a) xs) = do
  Refl <- f `eqT` (typeRep :: TypeRep [])
  return (Dyn a (head xs))
dynHead _ = Nothing

If we pattern match on the list constructor directly, we can pattern match on the list directly too!

import GHC.Types (type (~~))

pattern List :: () => [] ~~ t => TypeRep t
pattern List <- (eqT (typeRep @(Type -> Type) @[]) -> Just HRefl)
  where List = typeRep @(Type -> Type) @[]

dynHead :: Dynamic -> Maybe Dynamic
dynHead = \case
  Dyn (List :<->: a) (x:_) -> 
    Just (Dyn a (head xs))
  _ -> Nothing

Look how neat this looks! (apart from the :<->: noise)

pattern Pair :: () => (,) ~~ b => TypeRep b
pattern Pair <- (eqT (typeRep @(Type -> Type -> Type) @(,)) -> Just HRefl)
  where Pair = typeRep @(Type -> Type -> Type) @(,)

dynSwap :: Dynamic -> Maybe Dynamic
dynSwap (Dyn (Pair :<->: a :<->: b) (x, y)) = Just (Dyn (Pair :<->: b :<->: a) (y, x))
...

(dynSwap does not compile without a type signature, is this a bug?)

or

pattern Pair_ :: () => ab ~ (a, b) => T a -> T b -> T ab
pattern Pair_ a b = Pair :<->: a :<->: b

dynSwap :: Dynamic -> Maybe Dynamic
dynSwap (Dyn (Pair_ a b) (x, y)) = Just (Dyn (Pair_ b a) (y, x))

It would be great if we didn't have to create new pattern synonym for each ruddy type constructor so it would be great if we could define Con and use visible type application proposed by #11350

pattern Con :: forall (u :: k1) (b :: k2). TypeRep u => u ~~ b => TypeRep b
pattern Con <- (eqT (typeRep @k1 @u) -> Just HRefl)
  where Con = typeRep @k1 @u

dynHead (Dyn (Con @[] :<->: a) (x:_)) = Just (Dyn a (head xs))

dynSwap (Dyn (Con @(,) :<->: a :<->: b) (x, y)) = Just (Dyn (Con @(,) :<->: b :<->: a) (y, x))

isPairOfIntAndFloat (Dyn (Con @(,) :<->: Con @Int :<->: Con @Float)) = True
isPairOfIntAndFloat _ = False

[Icelandjack]

dynHead :: Dynamic -> Maybe Dynamic
dynHead (Dyn (rxs :: TypeRep txs) (xs :: txs)) = do
  App rl rx <- splitApp rxs
  Refl <- rl `eqT` (typeRep :: TypeRep [])
  return (Dyn rx (head xs))

can look nicer

pattern (:<->:) :: () => fa ~ f a => TypeRep f -> TypeRep a -> TypeRep fa
pattern f :<->: a <- (splitApp -> Just (App f a))
  where f :<->: a = TypeApp f a

dynHead :: Dynamic -> Maybe Dynamic
dynHead (Dyn (f :<->: a) xs) = do
  Refl <- f `eqT` (typeRep :: TypeRep [])
  return (Dyn a (head xs))
dynHead _ = Nothing

If we pattern match on the list constructor directly, we can pattern match on the list directly too!

import GHC.Types (type (~~))

pattern List :: () => [] ~~ t => TypeRep t
pattern List <- (eqT (typeRep @(Type -> Type) @[]) -> Just HRefl)
  where List = typeRep @(Type -> Type) @[]

dynHead :: Dynamic -> Maybe Dynamic
dynHead = \case
  Dyn (List :<->: a) (x:_) -> 
    Just (Dyn a (head xs))
  _ -> Nothing

Look how neat this looks! (apart from the :<->: noise)

pattern Pair :: () => (,) ~~ b => TypeRep b
pattern Pair <- (eqT (typeRep @(Type -> Type -> Type) @(,)) -> Just HRefl)
  where Pair = typeRep @(Type -> Type -> Type) @(,)

dynSwap :: Dynamic -> Maybe Dynamic
dynSwap (Dyn (Pair :<->: a :<->: b) (x, y)) = Just (Dyn (Pair :<->: b :<->: a) (y, x))
...

(dynSwap does not compile without a type signature, is this a bug?)

or

pattern Pair_ :: () => ab ~ (a, b) => T a -> T b -> T ab
pattern Pair_ a b = Pair :<->: a :<->: b

dynSwap :: Dynamic -> Maybe Dynamic
dynSwap (Dyn (Pair_ a b) (x, y)) = Just (Dyn (Pair_ b a) (y, x))

It would be great if we didn't have to create new pattern synonym for each ruddy type constructor so it would be great if we could define Con and use visible type application proposed by #11350

pattern Con :: forall (u :: k1) (b :: k2). TypeRep u => u ~~ b => TypeRep b
pattern Con <- (eqT (typeRep @k1 @u) -> Just HRefl)
  where Con = typeRep @k1 @u

dynHead (Dyn (Con @[] :<->: a) (x:_)) = Just (Dyn a (head xs))

dynSwap (Dyn (Con @(,) :<->: a :<->: b) (x, y)) = Just (Dyn (Con @(,) :<->: b :<->: a) (y, x))

isPairOfIntAndFloat (Dyn (Con @(,) :<->: Con @Int :<->: Con @Float)) = True
isPairOfIntAndFloat _ = False

[goldfirere]

I can see the usefulness of :<->:, though I would spell it :@:. And, yes, we need visible type patterns.

As for dynSwap: no, it's not a bug. The pattern-match introduces an equality constraint, and therefore the return type cannot be inferred, according to the OutsideIn algorithm. In this case, however, the equality constraint affects only existentially-bound variables, so it probably is OK, but that would be an exception to the rule.

[goldfirere]

I can see the usefulness of :<->:, though I would spell it :@:. And, yes, we need visible type patterns.

As for dynSwap: no, it's not a bug. The pattern-match introduces an equality constraint, and therefore the return type cannot be inferred, according to the OutsideIn algorithm. In this case, however, the equality constraint affects only existentially-bound variables, so it probably is OK, but that would be an exception to the rule.

[Icelandjack]

Your plan adds a superclass to Typeable

class Typeable k => Typeable (a :: k)

but this proposal doesn't: which is the right one and will it require UndecidableSuperClasses?

[Icelandjack]

Your plan adds a superclass to Typeable

class Typeable k => Typeable (a :: k)

but this proposal doesn't: which is the right one and will it require UndecidableSuperClasses?

[goldfirere]

I'm +1 on the kind superclass, if the solver doesn't choke on it.

[goldfirere]

I'm +1 on the kind superclass, if the solver doesn't choke on it.

[bgamari]

Icelandjack notifications@github.com writes:

Your plan adds a superclass to Typeable

class Typeable k => Typeable (a :: k) where

but this proposal doesn't: which is the right one and does will it require UndecidableSuperClasses?

Indeed; I was discussing alternative designs with Stephanie this weekend
and this is one of them. It would require UndecidableSuperClasses as
well as some care in the Typeable solver (which I have yet to figure out).

[bgamari]

Icelandjack notifications@github.com writes:

Your plan adds a superclass to Typeable

class Typeable k => Typeable (a :: k) where

but this proposal doesn't: which is the right one and does will it require UndecidableSuperClasses?

Indeed; I was discussing alternative designs with Stephanie this weekend
and this is one of them. It would require UndecidableSuperClasses as
well as some care in the Typeable solver (which I have yet to figure out).

[nomeata]

This proposal has not attracted discussion for a while. Please consider submitting it to the Committee for discussion, if you think it is ready, or close it, if you have abandoned this proposal.

[nomeata]

This proposal has not attracted discussion for a while. Please consider submitting it to the Committee for discussion, if you think it is ready, or close it, if you have abandoned this proposal.

[treeowl]

Can we wrap this up? This is already in 8.2, right?

[treeowl]

Can we wrap this up? This is already in 8.2, right?

[bgamari]

Indeed it is in 8.2. Ultimately time ran out to both bring finish the implementation and continue pushing the proposal process forward, so we "grandfathered" this proposal in.

[bgamari]

Indeed it is in 8.2. Ultimately time ran out to both bring finish the implementation and continue pushing the proposal process forward, so we "grandfathered" this proposal in.

[Icelandjack]

I'll add a link for some use of a SDynamic like structure for interested readers: StackOverflow

We can use the same trick of delaying when a constraint is discovered to build the leaves of a memo trie for Typeable a => f a. Conceptually the leaves of the trie are each one of the following GDynamics.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Data.Typeable
import Control.Monad (liftM)

data GDynamic f where
    GDynamic :: Typeable a => f a -> GDynamic f

unGDynamic :: Typeable a => GDynamic f -> Maybe (f a)
unGDynamic (GDynamic f) = gcast f

When constructing the trie, we don't have the Typeable a instances needed to construct the GDynamics. We only have a TypeRep. Instead we will steal the Typeable a instance provided when the value is accessed. A GDynamic value up to a Typeable a instance is the TypeRep, ..

[Icelandjack]

I'll add a link for some use of a SDynamic like structure for interested readers: StackOverflow

We can use the same trick of delaying when a constraint is discovered to build the leaves of a memo trie for Typeable a => f a. Conceptually the leaves of the trie are each one of the following GDynamics.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Data.Typeable
import Control.Monad (liftM)

data GDynamic f where
    GDynamic :: Typeable a => f a -> GDynamic f

unGDynamic :: Typeable a => GDynamic f -> Maybe (f a)
unGDynamic (GDynamic f) = gcast f

When constructing the trie, we don't have the Typeable a instances needed to construct the GDynamics. We only have a TypeRep. Instead we will steal the Typeable a instance provided when the value is accessed. A GDynamic value up to a Typeable a instance is the TypeRep, ..