Types constructors and existential types

Question

Only polymorphic function can be applied to values of existential types. Those properties can be expressed by the corresponding quantifiers for expressions, and characterized by natural transformations.

Similarly, when we define a type constructor

data List a = Nil | Cons a (List a)

This type constructor works for all a whereas type families allows to have non uniform type constructors

type family TRes i o
type instance TRes Bool = String
type instance TRes String  = Bool

What natural transformation characterizes precisely this idea of "uniformity" at type level ?

Is there an equivalent of forcing naturality like we have at value level with rank-n types ?

ApplyNat :: (forall a. a -> F a) -> b -> F b

Benjamin Hodgson Benjamin Hodgson · Accepted Answer · 2017-04-20T21:03:33

I think you've confused a couple of different ideas here.

This type constructor works for all a.

That's totality. List :: * -> * produces a valid type of kind * given any argument a of kind *. Haskell 98 datatypes are always total, but, as you point out, in modern Haskell you can write type families which don't cover all possible cases. TRes Int is not a "real" type, in the sense that it contains no values, it doesn't reduce to any other type, and it's not equal to any type other than TRes Int.

Haskell has no totality checker at the value level or the type level (apart from the rules about undecidable instances, which are a blunt instrument), so, just as there is no way to rule out undefined values, there is no way to rule out "stuck" type families like TRes Int. (For more on "stuck" type families see this blog post by Richard Eisenberg, the designer of TypeInType.)

Naturality is an altogether different idea. In value-level Haskell, a natural transformation between f and g is a polymorphic function mapping values of type f x to values of type g x, without knowing anything about x.

type f ~> g = forall x. f x -> g x

With GHC 8 and TypeInType we can talk about kinds using the same language we use to talk about types, because kinds are types. The type expression forall x. f x -> g x has kind * ((~>) :: forall k. (k -> *) -> (k -> *) -> *), so it's a perfectly valid classifier for types as well. A type with that kind is a polymorphic type function mapping types of kind f x to types of kind g x.

What would you use a type-level natural transformation for, in the real world? I dunno. You wouldn't, probably.

Types constructors and existential types

1 Answers