Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Where Do Type Systems Come From?

blog.felipe.rs

Post reply on HN
Print view View original

51–60 of 171 posts

Re: Where Do Type Systems Come From?

#51

Post by z1mm32m4n »

a-nikolaev wrote: post #47

Watch Oregon Programming Language School lectures "Basic Proof Theory" by Frank Pfenning. https://www.cs.uoregon.edu/research/summerschool/summer15/cu... Very clean and easy to follow video lectures on the relation between, types, programs, and logical proofs. One does not need functors and monoids to appreciate the beauty of functional type systems. (And to see why such type systems are indeed discovered rather than…

I second this. Frank's material is always thorough and approachable. He's designed and taught many courses at CMU, and his lecture notes for them are never less than impeccable.

Re: Where Do Type Systems Come From?

#52

Post by georgewsinger »

Nice article. I especially liked:

> program3 fails because runFunction can only run first-order functions and runFunction is a second-order function – a function that takes a first-order function as a parameter.

Here I had no idea that JavaScript implicitly typed `runFunction` that way. That's cool.

Also, I never thought of "higher-order functions" as breaking into a countable hierarchy of nth-order functions, which is an interesting thought. In Haskell the hierarchy would start off as

    zerothOrderFunction :: a
    firstOrderFunction :: a -> b
    SecondOrderFunction :: a -> (b -> c)
    SecondOrderFunction' :: (a -> b) -> c
In general, an nth-order function is a function which either

1. Takes an (n-1)th order function as an input and returns a simple type.

2. Takes a simple type as an input and returns an (n-1)th order function as an output.

The upshot is that typed programming languages not only catch bugs, but prevent you from legally expressing many non-sensical expressions (analogous to the set theory paradoxes). For example, consider the expression

    (\x -> x x) (\x -> x x)
If you expand this expression, it reduces to itself:

    (\x -> x x) (\x -> x x) == (\x -> x x) (\x -> x x)
In a purely untyped language, this expression would be legal. But what would be its meaning? Arguably, it is non-sense, and should be excluded from the set of legally expressible expressions. The way to do this is through a type system. And indeed, if you typed this statement into a Haskell REPL you would get a type error; this statement can actually be proven to be untypable (IIRC).

On the other hand, this means that typed systems are in some sense strictly less expressive than their untyped counterparts. It would therefore be interesting if somebody found an expression which was both (i) meaningful and (ii) only expressible in an untyped language. You would then have an argument for untyped languages :-)

Re: Where Do Type Systems Come From?

#53

Post by AnimalMuppet »

swsieber wrote: post #28
zzzcpan wrote: post #13

"Even though theoretically, type theories and type systems are not enough to prevent all the problems in logic and programming, they can be improved and refined to prevent an increasingly number of problems in the practice of logic and programming." It's actually just a belief. Nothing suggests that type systems and type theories can be improved to be practical at preventing bugs. I'd say it's the opposite, even with…

There are type systems that prevent race issues, use after free, and null pointer exceptions. So saying that they aren't practical at solving bugs is a little disingenuous.

Well... how much of actual software is written using those type systems? Less than 1%? So such type systems might be able to prevent bugs, but in practice, they don't.

Why aren't they used? Probably existing code bases, inertia, and ignorance play a role. I suspect, though, that at least part of the problem is that most programmers find those type systems too hard to use. In that sense, the type systems aren't practical.

And if you're going to blame the programmers for that, well, if your plan for making programming better requires different programmers than the ones we have, your plan isn't very practical, either.

Re: Where Do Type Systems Come From?

#56

Post by kmill »

georgewsinger wrote: post #52

Nice article. I especially liked: > program3 fails because runFunction can only run first-order functions and runFunction is a second-order function – a function that takes a first-order function as a parameter. Here I had no idea that JavaScript implicitly typed `runFunction` that way. That's cool. Also, I never thought of "higher-order functions" as breaking into a countable hierarchy of nth-order functions, which…

> > program3 fails because runFunction can only run first-order functions and runFunction is a second-order function – a function that takes a first-order function as a parameter. > Here I had no idea that JavaScript implicitly typed `runFunction` that way. That's cool.

In case it's not clear, it's just that it eventually ends up with a run time error (the talk about runFunction being a second-order function is just an explanation for why you should expect it to end up with a run time error). The evaluation is

       program3()
    == runFunction(runFunction)
    == runFunction(1)
    == 1(1)
    == Error: func (with value 1) is not a function

Re: Where Do Type Systems Come From?

#57

Post by gizmo686 »

georgewsinger wrote: post #52

Nice article. I especially liked: > program3 fails because runFunction can only run first-order functions and runFunction is a second-order function – a function that takes a first-order function as a parameter. Here I had no idea that JavaScript implicitly typed `runFunction` that way. That's cool. Also, I never thought of "higher-order functions" as breaking into a countable hierarchy of nth-order functions, which…

>On the other hand, this means that typed systems are in some sense strictly less expressive than their untyped counterparts. It would therefore be interesting if somebody found an expression which was both (i) meaningful and (ii) only expressible in an untyped language. You would then have an argument for untyped languages :-)

Any type system will reject some correct program. As a trivial example, consider:

    if( f() ):
        1 + "a"
    else
        1
This is a perfectly fine expression iff the result of f() is always false.

Re: Where Do Type Systems Come From?

#58

Post by glangdale »

zzzcpan wrote: post #13

"Even though theoretically, type theories and type systems are not enough to prevent all the problems in logic and programming, they can be improved and refined to prevent an increasingly number of problems in the practice of logic and programming." It's actually just a belief. Nothing suggests that type systems and type theories can be improved to be practical at preventing bugs. I'd say it's the opposite, even with…

Incendiary though the phrasing is, I'm halfway inclined to agree with you. There's a lot to be said for a solid, simple strong typing system. But some of the more sophisticated type systems that I either seen or read research literature about (I had a colleague who was doing PhD research in 'refinement types') are seem like they are hitting diminishing returns for programmer ease-of-use while catching an ever-diminishing number of bugs.

If you allotted me a finite amount of effort to put a codebase (a) into a strong type system, (b) festoon it with lots of pre- and post-conditions and asserts, (c) run it through every static checker under the sun, (d) build a huge suite of tests, (e) find a way to formally verify critical algorithms in it with (say) Z3, (f) carry out fuzz testing, ... I'd probably say "do the easy stuff from most of these categories" rather than "pick the One True Path and figure that that will save you from all your bugs".

Re: Where Do Type Systems Come From?

#59

Post by aoeusnth1 »

chroem- wrote: post #22
dungle6 wrote: post #16

Earlier quoted context omitted.

Lolwut?

He's right. The current type theory crazy is just another in a long line cargo cult programming fads. First it was pure OOP for everything, then it was pure FP for everything, and now it's types for everything. Yes they can be useful, but it's disingenuous to act like they're a cure-all. Most bugs aren't type related, and you're adding additional mental overhead with these extremely elaborate type systems.

I think you misread OP, and also misread the comment he was replying to; or, you just needed an excuse to vent about type systems.

Re: Where Do Type Systems Come From?

#60

Post by georgewsinger »

kmill wrote: post #56
georgewsinger wrote: post #52

Nice article. I especially liked: > program3 fails because runFunction can only run first-order functions and runFunction is a second-order function – a function that takes a first-order function as a parameter. Here I had no idea that JavaScript implicitly typed `runFunction` that way. That's cool. Also, I never thought of "higher-order functions" as breaking into a countable hierarchy of nth-order functions, which…

> > program3 fails because runFunction can only run first-order functions and runFunction is a second-order function – a function that takes a first-order function as a parameter. > Here I had no idea that JavaScript implicitly typed `runFunction` that way. That's cool. In case it's not clear, it's just that it eventually ends up with a run time error (the talk about runFunction being a second-order function is just…

I see. The error makes sense now.
Post reply on HN