[HN Gopher] Type Checking as Calculation
       ___________________________________________________________________
        
       Type Checking as Calculation
        
       Author : MississippiGary
       Score  : 11 points
       Date   : 2022-02-16 04:52 UTC (18 hours ago)
        
 (HTM) web link (billwadge.com)
 (TXT) w3m dump (billwadge.com)
        
       | josephcsible wrote:
       | > 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.
        
         | smaddox wrote:
         | 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.
        
           | josephcsible wrote:
           | But does PyFL actually use Self Types rigorously, or is this
           | only working because there's a hole in the type system?
        
           | bmc7505 wrote:
           | 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.
        
       | tromp wrote:
       | > 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 = lnlf.n(lfln.n(f(lflx.n f(f x))))(lx.f)(lx.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
        
       ___________________________________________________________________
       (page generated 2022-02-16 23:02 UTC)