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

111–120 of 171 posts

Re: Where Do Type Systems Come From?

#111

Post by agumonkey »

igravious wrote: post #39
agumonkey wrote: post #31

Earlier quoted context omitted.

Do not worry I understand 99% of your message. It's indeed a land far far away from the everyday coding of the majority of programmers. Unless they start digging, which I did. If you take code as data (lisp roots showing) you start to want to reason about it and quickly you end up reading about FP, denotations, different forms of evaluations, the value of metadata (type or else). Now I believe there's an artificial s…

I am delighted you responded so positively to what I wrote and didn't take what I wrote negatively which you could easily have done. Let's for arguments sake say that there are two camps (broadly speaking), the pragmatists as you say and the theorists/idealists let's call them. It reminds me of the difference between someone like Torvalds and someone like Stallman. Thing is we need both! You're right, the split _is_…

A guy tried to make a C-level formal language, even sexp based at first. After years he quit, saying it's probably impossible to have both (he wrote a long long article about the reasons, he didn't leave without explaining every problems in details).

Usually ideas filters in tiny bits, kind like genes. See closures, forever in lisp, but now in every languages while lisp is still niche.

The issue with theorists is that they see the world in abstract algebra / combinatorics, it's not fluff, it's just extremely high level thinking with extremely short notation[1]. It looks like straight BS until you spend enough time seeing that it translates into reality. Say something like prolog, where a few rules give you graph coloring. It's not theory only, it's actual application of different semantics.

[1] also, as in any group, they developped a culture and taste for some things, expressing everything in the form of arithmetic expressions. F^n <= iteration of F n times, it's a loop in average coder lingo.

Re: Where Do Type Systems Come From?

#113

Post by lower »

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…

Your definition of order is not the standard one!

Usually one would have:

    zerothOrderFunction :: a
    firstOrderFunction :: a -> b
    firstOrderFunction' :: a -> (b -> c)
    SecondOrderFunction :: (a -> b) -> c
After all, the functions firstOrderFunction and firstOrderFunction' are the same up to currying.

The standard definition of order is given here (at the end of the section):

https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus#T...

Re: Where Do Type Systems Come From?

#114

Post by heavenlyblue »

gizmo686 wrote: post #66
georgewsinger wrote: post #61

Earlier quoted context omitted.

Interesting. It could still be argued this program isn't meaningful (or perhaps "not useful").

Well, it is a trivial example. In reality, such things would be hidden in the complexity of the code. One could argue that if the correctness of the code cannot be accepted by the type system then it would also be confusing for a human to look at, and should therefor be refactored; which is why (in practice) this is a non issue. For a less trivial example, consider the expression "f(x) + g(x)" where both f and g can…

    "f(x) + g(x)"
This example is way too trivial to explain why type systems are generally undecidable. Let's imagine:

    def f/g(x):
      if isinstance(x, str):
       return 6
      elif isinstance(x, int):
       return 'a'
It is decidable for any type of x that is previously known. More importantly, type systems were essentially created to be able to prove whether a given expression is decidable or not.

    x = 1
    print_int(x)
    x="a"
    print_string(x)
This is solved by A-normal form (https://en.wikipedia.org/wiki/A-normal_form). Or by a more general concept that is available outside functional languages, SSA (https://en.wikipedia.org/wiki/Static_single_assignment_form).

You can make a point that this code is hard to modify in dynamic languages, but it is an issue with the code style rather than type systems. For example - IntelliJ IDEA would highlight such Pythonic code as incorrectly typed, since you have changed the type and therefore the variable itself.

I find the general argument against complexities in the type systems such as Haskell to be quite amusing, to be fair. Most of the time you are not dealing with code that is undecidable - and that's why type systems are interesting.

Re: Where Do Type Systems Come From?

#115

Post by heavenlyblue »

gizmo686 wrote: post #94
zem wrote: post #92

Earlier quoted context omitted.

the point is that just because two variables have the same name doesn't mean they are the same variable; you need a (name, scope) pair to fully disambiguate them. some languages have the scope of a name be the enclosing function, so that all references to x within a function body are the same x, and the type therefore attaches to (x, function). however that is not the only way to do it; in ocaml the let statement reb…

Yes, my point is that the fact that "x" refers to two different variables is a feature of the language, not the type system.

    f(x) + g(x)
For any type of x is enumerable. What that means is that for this specific expression, you can enumerate all of the types that x may take, and then enumerate all of the types that a function would return, given the types (if you can). You can then decide whether this expression is true or not.

Now it depends on the implementation of f and g. And type systems, in most of the practical cases - would be able to deal with this.

    x = 1
    print_int(x)
    x="a"
    print_string(x)
The second example is always decidable, if we agree that semantics of '=' are generally a question of equivalence.

Re: Where Do Type Systems Come From?

#116

Post by coldtea »

kronos29296 wrote: post #112

Nice article about type theory. > Why there’s so much research around types if perfectly applying them to programming languages is impractical? Somehow Haskell does this perfectly. Whaddya say to that?

I say, citation needed. Who said "Haskell does it perfectly"?

Not to mention the mental overhead of Haskell (which is also not optimal).

Re: Where Do Type Systems Come From?

#117

Post by coldtea »

igravious wrote: post #24
pier25 wrote: post #4

Reminded me of Gödel's incompleteness theorems. First incompleteness theorem Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F. Second incompleteness theorem For any consistent system F within which a certain amount of elementary arithmetic can be carried…

Honest question. What in the article prompted you to think about Gödel and his theorems? Why were you reminded?

For one, Godel used the same kind of self-referential statements described in the article ("this proposition is not provable" etc) and used math to create a kind of enumeration of propositions and have the proposition refer to itself.

Re: Where Do Type Systems Come From?

#118

Post by coldtea »

smcl wrote: post #2

I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. I get that these underpin the technology we as programmers use every single day, but I'm a little ashamed that I can't get excited about the subject and feel like it's too late for me to bother trying.

>I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems.

Not even 1/10th of HN has that. Tons of business types, lowly JS programmers, designers, sys-admin types, old-school programmers in C/C++, etc around.

Re: Where Do Type Systems Come From?

#120

Post by skywhopper »

igravious wrote: post #24
pier25 wrote: post #4

Reminded me of Gödel's incompleteness theorems. First incompleteness theorem Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F. Second incompleteness theorem For any consistent system F within which a certain amount of elementary arithmetic can be carried…

Honest question. What in the article prompted you to think about Gödel and his theorems? Why were you reminded?

I spent the whole article wondering when Gödel would be mentioned, and was disappointed that he wasn't given that the Incompleteness Theorem was at least partly a response to Russell's work, and because it applies directly to computer systems. The conclusions Gödel reached are asserted in the article but not cited which is weird given the other references.
Post reply on HN