Difference between revisions of "Hask"
m (→The seq problem: Format) 
(Rewrite) 

Line 1:  Line 1:  
−  '''Hask''' is the name usually given to the [[Category theorycategory]] having Haskell types as objects and Haskell functions between them as morphisms. 

+  '''Hask''' refers to a [[Category theorycategory]] 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. 

−  A typeconstructor that is an instance of the Functor class is an endofunctor on Hask. 

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

−  A solution approach to the issue of partiality making many of the identities required by categorical constructions not literally true in Haskell: 

+  { class="wikitable" 

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

⚫  
+   For any functions 

+  <hask>f :: a > r</hask> 

+  <hask>g :: b > r</hask> 

⚫  
+  there is a unique function 

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

−  == The seq problem == 

+  such that: 

+  <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 _ = ()</hask> 

+   <hask>u2 _ = undefined</hask> 

+   

+  ! scope="row"  Difference 

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

+  } 

−  The right identity law fails in '''Hask''' if we distinguish values which can be distinguished by <hask>seq</hask>, since: 

+  == Platonic '''Hask''' == 

−  <hask>id . undefined = \x > id (undefined x) = \x > undefined x</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. 

−  should be equal to <hask>undefined</hask>, but can be distinguished from it using <hask>seq</hask>: 

+  == Links == 

⚫  
⚫  
⚫  
−  * Exception: Prelude.undefined 

−  
−  
⚫  
−  () 

−  
−  == 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) 

−  
⚫  
⚫  
−  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.
Initial Object  Terminal Object  Sum  Product  

Definition  There is a unique function

There is a unique function

For any functions
there is a unique function
such that:

For any functions
there is a unique function
such that:

Platonic candidate  u1 r = case r of {}

u1 _ = ()

u1 (Left a) = f a

u1 r = (f r,g r)

Example failure condition  r ~ ()

r ~ ()

r ~ ()

r ~ ()

Alternative u  u2 _ = ()

u2 _ = undefined

u2 _ = ()

u2 _ = undefined

Difference  u1 undefined = undefined

u1 _ = ()

u1 undefined = undefined

u1 _ = (undefined,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.