Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
hask [2015/12/16 22:00] nikolaj |
hask [2016/05/10 18:27] nikolaj |
||
|---|---|---|---|
| Line 19: | Line 19: | ||
| ($\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'. | ||
