Observations

Seems like the site does not exist anymore. Sad. 

Just discovered this company, which is in Paris. Really impressed. https://www.tweag.io/about
 

https://github.com/qfpl/zippers 

on SO

TLDR:  there's no way you can define in set theory a function that does not return a result. (Actually you can, but then the whole sets axiomatics should be overhauled.)

true x y = x
false x y = y

lampair :: a -> b -> (a -> b -> c) -> c
lampair x y p = p x y

pa :: ((a -> b -> c) ->c) -> a
pa p = p true

And I see

   • Couldn't match type ‘a’ with ‘c’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          pa :: forall a b c. ((a -> b -> c) -> c) -> a
        at sample1.hs:8:1-30
      ‘c’ is a rigid type variable bound by
        the type signature for:
          pa :: forall a b c. ((a -> b -> c) -> c) -> a
        at sample1.hs:8:1-30
      Expected type: a -> b -> c
        Actual type: c -> b -> c
    • In the first argument of ‘p’, namely ‘true’
      In the expression: p true
      In an equation for ‘pa’: pa p = p true
    • Relevant bindings include
        p :: (a -> b -> c) -> c (bound at sample1.hs:9:4)
        pa :: ((a -> b -> c) -> c) -> a (bound at sample1.hs:9:1)
  |

What have I done wrong? What fails here? Is Hindley-Milner "not smart enough"? What am I missing?

Джавасприпт, Хаскель и Скала, и, говорят, OCaml, из-за своей компактности, канают в качестве скриптовых языков.

Питон в этом смысле тоже ничо, но там, во-первых, споткнуться можно много где, во-вторых, на уровне компиляции нам ничего не скажут. Это уже на продакшене ебанется. То-то квора, которая на питоне, деплоится по сто раз в час (а тесты потом гоняют, и кодревью тоже). 

List a = Codensity Endo a = forall r. (a -> r -> r) -> r -> r

    nil :: List a
    nil = \f z -> z

    cons :: a -> List a -> List a
    cons x xs = \f z -> f x (xs f z)

    append :: List a -> List a -> List a
    append xs ys = \f z -> xs f (ys f z)

    foldr :: (a -> r -> r) -> r -> List a -> r
    foldr f z xs = xs f z

Basically, it's like lambda.

Src: https://golem.ph.utexas.edu/category/2012/09/where_do_monads_come_from.html#c042100

(10x _hacid_)

The list of references starts with Penrose.

author's page

http://r6.ca/blog/20110808T035622Z.html

"I would like to introduce you to a very general algorithm that I like to call the Gauss-Jordan-Floyd-Warshall-McNaughton-Yamada algorithm. With this simple algorithm (an algorithm whose implementation is not very much longer than its name) you can solve almost half of the problems you might encounter in computer science. For instance, this algorithm will let you:

- compute transitive closures
- compute shortest paths
- compute largest capacity paths
- compute most reliable paths
- compute the regular expression for a finite automaton
- solve linear equations
"