Difference between revisions of "Hask"

From HaskellWiki
Jump to navigation Jump to search
(Rewrite)
Line 1: Line 1:
−
'''Hask''' is the name usually given to the [[Category theory|category]] having Haskell types as objects and Haskell functions between them as morphisms.
 +
'''Hask''' refers to a [[Category theory|category]] with types as objects and functions between them as morphisms. However, its use is ambiguous. Sometimes it refers to Haskell (''actual Hask''), and sometimes it refers to some subset of Haskell where no values are bottom and all functions terminate (''platonic Hask''). The reason for this is that platonic Hask has lots of nice properties that actual Hask does not, and is thus easier to reason in.
   
  +
== Hask ==
−
A type-constructor that is an instance of the Functor class is an endofunctor on Hask.
  
   
  +
Actual Hask does not have sums, products, or an initial object, and <hask>()</hask> is not a terminal object. The Monad identities fail for almost all instances of the Monad class.
−
* [http://www.cs.gunma-u.ac.jp/~hamana/Papers/cpo.pdf Makoto Hamana: ''What is the category for Haskell?'']
  
   
  +
{| class="wikitable"
−
A solution approach to the issue of partiality making many of the identities required by categorical constructions not literally true in Haskell:
  
  +
|+ Why '''Hask''' isn't as nice as you'd thought.
  +
! scope="col" |
  +
! scope="col" | Initial Object
  +
! scope="col" | Terminal Object
  +
! scope="col" | Sum
  +
! scope="col" | Product
  +
|-
  +
! scope="row" | Definition
  +
| There is a unique function
  +
<hask>u :: Empty -> r</hask>
  +
| There is a unique function
  +
<hask>u :: r -> ()</hask>
  +
| For any functions
  +
<hask>f :: a -> r</hask>
  +
<hask>g :: b -> r</hask>
   
  +
there is a unique function
−
* [http://www.cs.nott.ac.uk/~nad/publications/danielsson-popl2006-tr.pdf Nils A. Danielsson, John Hughes, Patrik Jansson, and Jeremy Gibbons. ''Fast and loose reasoning is morally correct.'']
  
  +
<hask>u :: Either a b -> r</hask>
   
  +
such that:
  +
<hask>u . Left = f</hask>
  +
<hask>u . Right = g</hask>
  +
| For any functions
  +
<hask>f :: r -> a</hask>
  +
<hask>g :: r -> b</hask>
   
  +
there is a unique function
  +
<hask>u :: r -> (a,b)</hask>
   
  +
such that:
−
== The seq problem ==
  
  +
<hask>fst . u = f</hask>
  +
<hask>snd . u = g</hask>
  +
|-
  +
! scope="row" | Platonic candidate
  +
| <hask>u1 r = case r of {}</hask>
  +
| <hask>u1 _ = ()</hask>
  +
| <hask>u1 (Left a) = f a</hask>
  +
<hask>u1 (Right b) = g b</hask>
  +
| <hask>u1 r = (f r,g r)</hask>
  +
|-
  +
! scope="row" | Example failure condition
  +
| <hask>r ~ ()</hask>
  +
| <hask>r ~ ()</hask>
  +
| <hask>r ~ ()</hask>
  +
<hask>f _ = ()</hask>
  +
<hask>g _ = ()</hask>
  +
| <hask>r ~ ()</hask>
  +
<hask>f _ = undefined</hask>
  +
<hask>g _ = undefined</hask>
  +
|-
  +
! scope="row" | Alternative u
  +
| <hask>u2 _ = ()</hask>
  +
| <hask>u2 _ = undefined</hask>
  +
| <hask>u2 _ = ()</hask>
  +
| <hask>u2 _ = undefined</hask>
  +
|-
  +
! scope="row" | Difference
  +
| <hask>u1 undefined = undefined</hask>
  +
<hask>u2 undefined = ()</hask>
  +
| <hask>u1 _ = ()</hask>
  +
<hask>u2 _ = undefined</hask>
  +
| <hask>u1 undefined = undefined</hask>
  +
<hask>u2 undefined = ()</hask>
  +
| <hask>u1 _ = (undefined,undefined)</hask>
  +
<hask>u2 _ = undefined</hask>
  +
|- style="background: red;"
  +
! scope="row" | Result
  +
! scope="col" | FAIL
  +
! scope="col" | FAIL
  +
! scope="col" | FAIL
  +
! scope="col" | FAIL
  +
|}
   
  +
== Platonic '''Hask''' ==
−
The right identity law fails in '''Hask''' if we distinguish values which can be distinguished by <hask>seq</hask>, since:
  
   
  +
Because of these difficulties, Haskell developers tend to think in some subset of Haskell where types do not have bottoms. This means that it only includes functions that terminate, and typically only finite values. The corresponding category has the expected initial and terminal objects, sums and products. Instances of Functor and Monad are really endofunctors and monads.
−
<hask>id . undefined = \x -> id (undefined x) = \x -> undefined x</hask>
  
   
  +
== Links ==
−
should be equal to <hask>undefined</hask>, but can be distinguished from it using <hask>seq</hask>:
  
   
  +
* [http://www.cs.gunma-u.ac.jp/~hamana/Papers/cpo.pdf Makoto Hamana: ''What is the category for Haskell?'']
  +
* [http://www.cs.nott.ac.uk/~nad/publications/danielsson-popl2006-tr.pdf Nils A. Danielsson, John Hughes, Patrik Jansson, and Jeremy Gibbons. ''Fast and loose reasoning is morally correct.'']
   
−
ghci> <hask>(undefined :: Int -> Int) `seq` ()</hask>
  
−
* Exception: Prelude.undefined
  
−  
−  
−
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}}
  
 
[[Category:Mathematics]]
  
[[Category:Mathematics]]
 
[[Category:Theoretical foundations]]
  
[[Category:Theoretical foundations]]

Revision as of 10:23, 7 August 2012

Hask refers to a category with types as objects and functions between them as morphisms. However, its use is ambiguous. Sometimes it refers to Haskell (actual Hask), and sometimes it refers to some subset of Haskell where no values are bottom and all functions terminate (platonic Hask). The reason for this is that platonic Hask has lots of nice properties that actual Hask does not, and is thus easier to reason in.

Hask

Actual Hask does not have sums, products, or an initial object, and () is not a terminal object. The Monad identities fail for almost all instances of the Monad class.

Why Hask isn't as nice as you'd thought.
Initial Object Terminal Object Sum Product
Definition There is a unique function

u :: Empty -> r

There is a unique function

u :: r -> ()

For any functions

f :: a -> r g :: b -> r

there is a unique function u :: Either a b -> r

such that: u . Left = f u . Right = g

For any functions

f :: r -> a g :: r -> b

there is a unique function u :: r -> (a,b)

such that: fst . u = f snd . u = g

Platonic candidate u1 r = case r of {} u1 _ = () u1 (Left a) = f a

u1 (Right b) = g b

u1 r = (f r,g r)
Example failure condition r ~ () r ~ () r ~ ()

f _ = () g _ = ()

r ~ ()

f _ = undefined g _ = undefined

Alternative u u2 _ = () u2 _ = undefined u2 _ = () u2 _ = undefined
Difference u1 undefined = undefined

u2 undefined = ()

u1 _ = ()

u2 _ = undefined

u1 undefined = undefined

u2 undefined = ()

u1 _ = (undefined,undefined)

u2 _ = undefined

Result FAIL FAIL FAIL FAIL

Platonic Hask

Because of these difficulties, Haskell developers tend to think in some subset of Haskell where types do not have bottoms. This means that it only includes functions that terminate, and typically only finite values. The corresponding category has the expected initial and terminal objects, sums and products. Instances of Functor and Monad are really endofunctors and monads.

Links

Retrieved from "https://wiki.haskell.org/index.php?title=Hask&oldid=48008"