Type Checking as Calculation
billwadge.com
Type Checking as Calculation
1–7 of 7 posts
Re: Type Checking as Calculation
#2> 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.
Re: Type Checking as Calculation
#3> 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…
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.
Re: Type Checking as Calculation
#4> 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…
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.
Re: Type Checking as Calculation
#5> 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.
Re: Type Checking as Calculation
#6> 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…
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.
But does PyFL actually use Self Types rigorously, or is this only working because there's a hole in the type system?
Re: Type Checking as Calculation
#7> 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…
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.
To clarify: Kind is able to type lambda-encoded recursive data types with Self Types. This is something that is not possible in Haskell.