Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
hask [2015/12/16 22:00]
nikolaj
hask [2016/10/16 15:09]
nikolaj
Line 2: Line 2:
 ==== Note ==== ==== Note ====
 >​**todo:​** ​ >​**todo:​** ​
->Hask as category: 
-> 
 > objects are types > objects are types
 > >
Line 12: Line 10:
  
 ==== Discussion ==== ==== Discussion ====
 +Hask is the syntactic subset of Haskell which permits a whole bunch of operations that are seen in basic category theory.
 +
 With $\to$ and $\times$ etc., Hask is //almost// Cartesian closed. A particular problem is the polymorphic term '​undefined',​ which is defined to be term of every type. It prevents, for example, initial objects (i.e. there no analog to the "empty set"). Or when it comes to setting up the categorical product, the projections $\pi_1,​\pi_2$ couldn'​t distinguish between $'​(\text{undefined},​\text{undefined})'​$ and just $\text{undefined}$,​ spoiling uniqueness. See [[http://​www.haskell.org/​haskellwiki/​Hask|Hask]] for more examples. With $\to$ and $\times$ etc., Hask is //almost// Cartesian closed. A particular problem is the polymorphic term '​undefined',​ which is defined to be term of every type. It prevents, for example, initial objects (i.e. there no analog to the "empty set"). Or when it comes to setting up the categorical product, the projections $\pi_1,​\pi_2$ couldn'​t distinguish between $'​(\text{undefined},​\text{undefined})'​$ and just $\text{undefined}$,​ spoiling uniqueness. See [[http://​www.haskell.org/​haskellwiki/​Hask|Hask]] for more examples.
  
-Hask is the largest ​category ​of types in Haskell but you can find more well behaved categories. See also the [[http://​hackage.haskell.org/​package/​category-extras|category-extras]] package.+As far as some basic category theoretical concepts go, Hask is the largest ​collection ​of types in Haskell but by more restriction, ​you can find some actual and nicely ​behaved categories. See also the [[http://​hackage.haskell.org/​package/​category-extras|category-extras]] package.
  
 Another deficit is that when it comes to passing functions as arguments, Haskell sees more than just Hask morphisms. A nicer definition of the largest category of Haskell would be if arrows weren'​t Haskell functions identified by function extensionally ​ Another deficit is that when it comes to passing functions as arguments, Haskell sees more than just Hask morphisms. A nicer definition of the largest category of Haskell would be if arrows weren'​t Haskell functions identified by function extensionally ​
 ($\forall x. f(x)=g(x)\implies f=g$), ​ ($\forall x. f(x)=g(x)\implies f=g$), ​
 but rather identified if equivalent when passed to other Haskell functions as arguments ​ but rather identified if equivalent when passed to other Haskell functions as arguments ​
-($\forall h. h(f)=h(g)\implies f=g$, see indiscernibility of identicals ). +($\forall h. h(f)=h(g)\implies f=g$, see indiscernibility of identicals. We can back the first definition if we consider only the eval-functions for $h$'s). 
 However, this doesn'​t work: With the definition of concatenation given above, the category laws imply that '​(undefined :: Int -> Char).id'​ must be '\x ->​(undefined :: Int -> Char) x'. But there are functions which can detect the non-extensive property of '​undefined :: Int -> Char' being the '​undefined'​ term for the type 'Int -> Char'. The function '​seq'​ (which is implemented to make enforcement of strict evaluation possible) will return a different result when passed the extensionally equal functions '​undefined :: Int -> Char' and '\x ->​(undefined :: Int -> Char) x'​. ​ However, this doesn'​t work: With the definition of concatenation given above, the category laws imply that '​(undefined :: Int -> Char).id'​ must be '\x ->​(undefined :: Int -> Char) x'. But there are functions which can detect the non-extensive property of '​undefined :: Int -> Char' being the '​undefined'​ term for the type 'Int -> Char'. The function '​seq'​ (which is implemented to make enforcement of strict evaluation possible) will return a different result when passed the extensionally equal functions '​undefined :: Int -> Char' and '\x ->​(undefined :: Int -> Char) x'​. ​
  
Link to graph
Log In
Improvements of the human condition