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