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

161–170 of 171 posts

Re: Where Do Type Systems Come From?

#161

Post by johncolanduoni »

catnaroek wrote: post #160
johncolanduoni wrote: post #157

Earlier quoted context omitted.

If your standard for a possible programming language that supports concurrency is that no data races are possible, then there's very few languages to be had.

This particular discussion wasn't about ruling out data races (although, of course, that is important too). It was about ruling out trying to read a list of strings from a reference cell containing a list of ints.

You're the one who brought up threads as a reason runtime monomorphisation doesn't work. If access to the list is properly synchronized, then what I proposed works just fine (you get your runtime error in whatever thread accesses the list second). If it's not, then unless you're using a concurrent data structure you're already screwed. The type system will at most change exactly how you get screwed.

Re: Where Do Type Systems Come From?

#162

Post by kazinator »

Animats wrote: post #138

There's another approach, from Boyer and Moore. Boyer and Moore built up mathematics from constructs at the Peano axiom level (zero, add1, etc.) plus recursive functions that must terminate. It's constructive mathematics; there are no quantifiers, no ∀ or ∃. [1] They built an automatic theorem prover in the 1970s and 1980s that works on this theory. (I recently made it work on Gnu Common LISP and put it on Github, so…

If every operation can have any type arguments applied to it and does something sensible with no compiler or run-time error ... good luck debugging, surely.

What happens with OOP? Every class has to understand how to "bark", not only the dog class?

If any class can somehow "bark" without throwing an exception, that may not be in alignment with the programmer's intent, or promote the furtherance of his or her goals in any way.

For intance, the intent may be that the programmer wanted to ask the local variable dog to "bark", but misspelled it as ndog and the integer which counts the number of dogs was asked to bark instead.

There is much value in identifying the problem that an integer doesn't bark.

Re: Where Do Type Systems Come From?

#163

Post by Animats »

kazinator wrote: post #162
Animats wrote: post #138

There's another approach, from Boyer and Moore. Boyer and Moore built up mathematics from constructs at the Peano axiom level (zero, add1, etc.) plus recursive functions that must terminate. It's constructive mathematics; there are no quantifiers, no ∀ or ∃. [1] They built an automatic theorem prover in the 1970s and 1980s that works on this theory. (I recently made it work on Gnu Common LISP and put it on Github, so…

If every operation can have any type arguments applied to it and does something sensible with no compiler or run-time error ... good luck debugging, surely. What happens with OOP? Every class has to understand how to "bark", not only the dog class? If any class can somehow "bark" without throwing an exception, that may not be in alignment with the programmer's intent, or promote the furtherance of his or her goals in…

Boyer-Moore theory has "shells", which are like structures. See page 39 of [1]. Since this is a pure functional language, values cannot be altered. Shells have constructors, a type predicate, and can have restriction predicates on values.

    Shell Definition.
    Add the shell ADD1 of one argument
    with bottom object (ZERO),
    recognizer NUMBERP,
    accessor SUB1,
    type restriction (NUMBERP X1),
    default value (ZERO), and
    well-founded relation SUB1P.
It's not intended that you run programs in Boyer-Moore theory, although you can. It's a proof tool.

[1] https://www.cs.utexas.edu/users/boyer/acl.pdf

Re: Where Do Type Systems Come From?

#164

Post by kazinator »

Animats wrote: post #163
kazinator wrote: post #162

Earlier quoted context omitted.

If every operation can have any type arguments applied to it and does something sensible with no compiler or run-time error ... good luck debugging, surely. What happens with OOP? Every class has to understand how to "bark", not only the dog class? If any class can somehow "bark" without throwing an exception, that may not be in alignment with the programmer's intent, or promote the furtherance of his or her goals in…

Boyer-Moore theory has "shells", which are like structures. See page 39 of [1]. Since this is a pure functional language, values cannot be altered. Shells have constructors, a type predicate, and can have restriction predicates on values. Shell Definition. Add the shell ADD1 of one argument with bottom object (ZERO), recognizer NUMBERP, accessor SUB1, type restriction (NUMBERP X1), default value (ZERO), and well-foun…

I will have to read this to understand what we can prove with this; or rather, what kinds of wrongs in a program under this theory are usefully proved to be false.

---

Ouch; did you see that "overfull hbox" that got rendered out in the first line of paragraph 3 of the Preface? :)

Re: Where Do Type Systems Come From?

#165

Post by cel1ne »

didibus wrote: post #109
cel1ne wrote: post #97

Earlier quoted context omitted.

> It is often very useful to structure different types of data together in a common structure. "Very useful" often just means: coding a properly typed, easily-understandable solution takes longer than doing it untyped. I argue that is the case only when using a plain-text editor. When you have a good IDE for a typed-language at hand that can refactor, complete, analyed and follow code on the press of a button, you lo…

How do you define expressiveness? To me, it means saying more with less. Applied to code it means doing more with less work. Which directly translates to productivity gains. Now, what IDE and language are you referring too? The best one I've used was VisualStudio for C#. While I'd say typing wasn't adding too much overhead in it, its type system is also poor, and it's arguable that it may not really prevent much bugs…

IDEA with Kotlin or Java is fantastic.

Re: Where Do Type Systems Come From?

#166

Post by jonsterling »

ky3 wrote: post #64
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…

foo :: a -> (b -> c) Not saying it's wrong, but "foo is a second-order function" is a distinctly minority opinion. To a useful first approximation, Haskell works as a cartesian-closed category, which basically means we have tuples and that tuples harmonize with functions so that foo behaves just like uncurry foo :: (a,b) -> c which is a first-order function. So the majority opinion calls foo a first-order arity-2 fun…

I think it is not just a minority opinion, but just plain wrong.

Re: Where Do Type Systems Come From?

#167

Post by kazinator »

leshow wrote: post #152
z3t4 wrote: post #148

Earlier quoted context omitted.

ive only used vbscript and javascript extensibly. when ive tried java and #C ive been annoyed by the verbosity of types. and when looking at haskel or ocaml im just confused. for me types are an optimization or extra documentation for undescriptive naming, like str x, int y, list z. vs. name,age,friends. so i want to know what im missing, will there be less bugs and regressions? will i be more productive ?

> for me types are an optimization or extra documentation for undescriptive naming, This is one of those things where you should try to reserve judgement about it because your experience is so limited. Modern typed languages often don't even require you to write the type, because of type inference. > will there be less bugs and regressions? will i be more productive ? The idea with static analysis is that you're push…

Speaking of adding to a number, in some dynamic languages, you can add 3/5 to 7/5 and the result will be 2, of type integer, indistinguishable from the object produced by a literal 2. That 3/5 and 7/5 come from some run-time source, so the result type can't be statically hard-coded to integer or rational or whatever. And so now on the static side you're into variant types and "maybes" and other junk creating an incomprehensible soup which basically Greenspuns dynamic typing in a way that will get your name cursed by subsequent maintainers.

Re: Where Do Type Systems Come From?

#168

Post by winter_blue »

"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. That means the research for better practical type systems is far from over!"

This is great point, and I think it is absolutely worthwhile to put time into researching better, more powerful type systems.

Tony Hoare said[1] that his research into formal systems and his hope that the pr Framing world would embrace these new innovations that increase safety and reliability was futile, but I think what we need is a new approach, with particular care given to practicality and adoptability.

[1] https://en.wikipedia.org/wiki/Tony_Hoare

Re: Where Do Type Systems Come From?

#169

Post by leshow »

kazinator wrote: post #167
leshow wrote: post #152

Earlier quoted context omitted.

> for me types are an optimization or extra documentation for undescriptive naming, This is one of those things where you should try to reserve judgement about it because your experience is so limited. Modern typed languages often don't even require you to write the type, because of type inference. > will there be less bugs and regressions? will i be more productive ? The idea with static analysis is that you're push…

Speaking of adding to a number, in some dynamic languages, you can add 3/5 to 7/5 and the result will be 2, of type integer, indistinguishable from the object produced by a literal 2. That 3/5 and 7/5 come from some run-time source, so the result type can't be statically hard-coded to integer or rational or whatever. And so now on the static side you're into variant types and "maybes" and other junk creating an incom…

I can't make heads or tails of what your criticism is. Algebraic types are wonderful, I find it difficult to code in a language without them. I'd hardly call it 'junk'.

Re: Where Do Type Systems Come From?

#170

Post by [deleted] »

naasking wrote: post #75
bykovich2 wrote: post #67

Earlier quoted context omitted.

"Practical" is the key word here, I believe.

A key word that had been disproven many times. The most recent example is Rust, which has a type checker that now type checks many previously unsafe C++ idioms. The other examples I listed are also quite practical, and have been used in high assurance systems.

[deleted]
Post reply on HN