(Add a section on limits failing to match up with Haskell datatypes)
m (→The seq problem: Format)
Revision as of 18:31, 7 February 2011
Hask is the name usually given to the category having Haskell types as objects and Haskell functions between them as morphisms.
A type-constructor that is an instance of the Functor class is an endofunctor on Hask.
A solution approach to the issue of partiality making many of the identities required by categorical constructions not literally true in Haskell:
- Nils A. Danielsson, John Hughes, Patrik Jansson, and Jeremy Gibbons. Fast and loose reasoning is morally correct.
1 The seq problemThe right identity law fails in Hask if we distinguish values which can be distinguished by
* Exception: Prelude.undefined
2 The limits problem
Even in the absence of seq, bottoms cause datatypes to not actually be instances of the expected categorical constructions. For instance, using some intuition from the category of sets, one might expect the following:
data Void -- no elements ; initial object data () = () -- terminal object data (a, b) = (a, b) -- product data Either a b = Left a | Right b -- coproduct
However, Void actually does contain an element, bottom, so for each
x :: T,
const x is a different function
Void -> T, meaning
Void isn't initial (it's actually terminal).
const undefined and
const () are two distinct functions into
t :: () -> Int t () = 5 t . const () = \x -> 5 t . const undefined = \x -> undefined
So, () is not terminal.
Similar issues occur with (co)products. Categorically:
\p -> (fst p, snd p) = id \s -> case s of Left x -> p (Left x) ; Right y -> p (Right y) = p
but in Haskell
id undefined = undefined /= (undefined, undefined) = (fst undefined, snd undefined) const 5 undefined = 5 /= undefined = case undefined of Left x -> const 5 (Left x) Right y -> const 5 (Right y)
This article is a stub. You can help by expanding it.