[Haskell-cafe] type metaphysics

[Dan Doel]

On Tuesday 03 February 2009 9:05:08 pm wren ng thornton wrote:
> Extending things to GADTs, this is also the reason why functions are
>
> called exponential and denoted as such in category theory:
> |N -> M| = |M| ^ |N|
>
> That's the number of functions that exist in that type. Not all of these
> are computable, however, as discussed elsewhere.

This is all correct, except that exponentials are just part of algebraic data 
types, not generalized algebraic data types. Generalized algebraic data types 
are similar to inductive families, in that you can target constructors at 
specific type-indices, like so:

  data T t where
    I :: T Int
    P :: T a -> T b -> T (a,b)

Both of those are genuine GADT constructors. There's also things like:

    E :: T a -> T b -> T b

But those are doable by 'mere' ADTs plus existential quantification:

  data T b = ... | forall a. P (T a) (T b)

-- Dan