Type Checking as Calculation | Hacker News Reader

Type Checking as Calculation

billwadge.com

> Could we still define factorial? This was the problem facing the developers of the lambda calculus (which doesn’t have built-in recursion).

Lambda calculus doesn't have built-in numbers either. Curiously, the standard representation of numbers in lambda calculus, the so-called Church numerals, allows for a non-recursive definition of factorial [1]:

fac = λnλf.n(λfλn.n(f(λfλx.n f(f x))))(λx.f)(λx.x)

> There’s more to type checking than Haskell’s rigid declarations.

I don't see such rigidity since most type declarations in Haskell can be omitted as they will be correctly inferred.

[1] https://flownet.com/ron/lambda-calculus.html

> In PyFL gone are all the things that ordinary people find difficult or downright weird: monads, mandatory currying, post- or prefix notation, pattern matching, etc. Instead infix notation and f(x,y,z) syntax for function application. The weird stuff has it’s proponents but PyFL proves it’s not inherently part of functional programming.

Textbook case of falling victim to the Blub Paradox.

> The answer is … int! Yes, PyFL has typed an untypable program!

I'm not sure why the author is making this sound like a good thing.

Totally agree about the Blub Paradox, but there's definitely value in Self Types. See, for example, [Kind](https://github.com/Kindelia/Kind), which is able to type recursive data types by using Self Types.

It should be noted that self types are non-trivial to implement and if one is not careful when using them, impredicativity can lead to inconsistent or undecidable definitions.

But does PyFL actually use Self Types rigorously, or is this only working because there's a hole in the type system?

To clarify: Kind is able to type lambda-encoded recursive data types with Self Types. This is something that is not possible in Haskell.

Reply on news.ycombinator.com