Type Checking as Calculation(billwadge.com)
billwadge.com
Type Checking as Calculation
https://billwadge.com/2022/02/16/type-checking-as-calculation/
2 comments
> 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.
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.
To clarify: Kind is able to type lambda-encoded recursive data types with Self Types. This is something that is not possible in Haskell.
But does PyFL actually use Self Types rigorously, or is this only working because there's a hole in the type system?
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