# Difference between revisions of "Hask"

(Add a section on limits failing to match up with Haskell datatypes) |
|||

Line 23: | Line 23: | ||

ghci> <hask>(id . undefined :: Int -> Int) `seq` ()</hask> |
ghci> <hask>(id . undefined :: Int -> Int) `seq` ()</hask> |
||

() |
() |
||

+ | |||

+ | == 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: |
||

+ | |||

+ | <haskell> |
||

+ | data Void -- no elements ; initial object |
||

+ | data () = () -- terminal object |
||

+ | |||

+ | data (a, b) = (a, b) -- product |
||

+ | data Either a b = Left a | Right b -- coproduct |
||

+ | </haskell> |
||

+ | |||

+ | However, Void actually does contain an element, bottom, so for each <code>x :: T</code>, <code>const x</code> is a different function <code>Void -> T</code>, meaning <code>Void</code> isn't initial (it's actually terminal). |
||

+ | |||

+ | Similarly, <code>const undefined</code> and <code>const ()</code> are two distinct functions into <code>()</code>. Consider: |
||

+ | |||

+ | <haskell> |
||

+ | t :: () -> Int |
||

+ | t () = 5 |
||

+ | |||

+ | t . const () = \x -> 5 |
||

+ | t . const undefined = \x -> undefined |
||

+ | </haskell> |
||

+ | |||

+ | So, () is not terminal. |
||

+ | |||

+ | Similar issues occur with (co)products. Categorically: |
||

+ | |||

+ | <haskell> |
||

+ | \p -> (fst p, snd p) = id |
||

+ | |||

+ | \s -> case s of Left x -> p (Left x) ; Right y -> p (Right y) = p |
||

+ | </haskell> |
||

+ | |||

+ | but in Haskell |
||

+ | |||

+ | <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) |
||

+ | </haskell> |
||

{{stub}} |
{{stub}} |

## Revision as of 05:20, 3 March 2010

**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:

## The seq problem

The right identity law fails in **Hask** if we distinguish values which can be distinguished by `seq`

, since:

`id . undefined = \x -> id (undefined x) = \x -> undefined x`

should be equal to `undefined`

, but can be distinguished from it using `seq`

:

ghci>`(undefined :: Int -> Int) `seq` ()`

* Exception: Prelude.undefined ghci>`(id . undefined :: Int -> Int) `seq` ()`

()

## 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).

Similarly, `const undefined`

and `const ()`

are two distinct functions into `()`

. Consider:

```
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.*