Where Do Type Systems Come From? • Hacker News Board

Re: Where Do Type Systems Come From?

#131

Post by johncolanduoni » Sat, Jul 08, 2017, 4:52 PM UTC

catnaroek wrote: post #90

evincarofautumn wrote: post #88

Earlier quoted context omitted.

It’s partly just coincidence that dynamically typed languages tend to have less expressive type systems. You could run any typechecker at runtime if you wanted. There’s no reason you couldn’t have a Python-like language where the “list” type dynamically keeps track of the types of its elements, function types keep track of the types of their inputs and outputs, and so on, to give you more precise & useful dynamic typ…

You create a reference cell containing an empty list. Because the cell is mutable, it can't have a polymorphic type - it must have a monomorphic one. How do you determine at runtime the type of this cell, before the first time you mutate it?

Why is that required? There's nothing stopping you from only giving the list a precise type after an element has been added. This mirrors the way statically typed languages with inference handle the same situation (except they wait for evidence that it's being used as a list of Ts, instead of the actual act).

Re: Where Do Type Systems Come From?

#132

Post by aleden » Sat, Jul 08, 2017, 5:02 PM UTC

aleden wrote: post #121

coldtea wrote: post #116

Earlier quoted context omitted.

I say, citation needed. Who said "Haskell does it perfectly"? Not to mention the mental overhead of Haskell (which is also not optimal).

Yeah, what the fuck? Most software engineers just want to get shit done quickly so they can go home to their wife and kids.

If you think this merits a downvote please tell why. Excuse my french.

Re: Where Do Type Systems Come From?

#133

Post by krallja » Sat, Jul 08, 2017, 5:54 PM UTC

sidlls wrote: post #129

krallja wrote: post #86

Earlier quoted context omitted.

Assembly languages are untyped. Nothing prevents you from reinterpreting a memory address as a type it is not. (Except possibly alignment issues.)

That's not quite right though, is it? Nothing prevents one from "creative" interpretation of memory in, say, C, either, but it would be difficult to argue C is untyped.

The C type system prevents you from accidental creative interpretation of memory. You wouldn't say Rust is untyped just because of the `unsafe` keyword either.

No such type safety exists in assembly, except that certain opcode-register combinations are prohibited.

Re: Where Do Type Systems Come From?

#134

Post by oldandtired » Sat, Jul 08, 2017, 6:06 PM UTC

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…

Depending on your system, 1(1) is quite sensible, That is applying 1 to a list of parameters just returns the 1st parameter. This is a matter of the semantics that one uses when application is run against any value.

1(1) -> 1

Just because the common idea of application is that it only applies to functions does not mean that application applied to other types is nonsensical and should end up with a runtime error.

If your language allows application to be defined for different types, then the type system should be capable of determining the type that returns from application.

A practical example of a language in which application is valid for integers is Unicon/Icon. Both functions and integers have specific semantics with regards to application. And failure is an option.

Re: Where Do Type Systems Come From?

#135

Post by alexashka » Sat, Jul 08, 2017, 6:08 PM UTC

naasking wrote: post #125

bogomipz wrote: post #84

Earlier quoted context omitted.

What I meant by basic was the description of types provided by a language - usually in an introductory text you might read when learning a new language. I probably didn't articulate that correctly. But I guess what I was referring to as a "middle ground"qa any resources for learning about types systems written in a similar approachable tone like this article. This was another article I read recently that I thought wa…

Types and Programming Languages is the go to book, and it's very accessible despite being a textbook: https://mitpress.mit.edu/books/types-and-programming-languag... You can find some earlier PDF drafts online if you Google.

I have the book and I must warn people, it is not THAT accessible - this is not evening reading for an hour, this is work.

Re: Where Do Type Systems Come From?

#136

Post by lists » Sat, Jul 08, 2017, 6:56 PM UTC

sgt101 wrote: post #128

Type Systems come from Russel - yup. But the notion of Type has an interesting origin in the west as well (I would love to read/understand histories of this concept from other cultures, but I am ignorant for now). My reading is that it was invented by Scotus as Haecceity ! This was required by Catholic Christianity because of the difficulty that The Creed introduces about the identity of God - there are three entitie…

> The fun bit it that this procession of thought is somewhat guessed at because writing things like this down or debating them publically was a quick route to the afterlife via a bonfire!

Theatre and Philosophy have always been able to have a lively chat with one another

Re: Where Do Type Systems Come From?

#137

Post by philix001 » Sat, Jul 08, 2017, 7:19 PM UTC

drc0 wrote: post #126

> That’s the equivalent of writing type annotations for programming functions. And the goal is avoiding bugs instead of logical contradictions. mh, given Curry–Howard correspondence, aren't those the same? so the goal is indeed not having logical contradictions?

They are. I avoided introducing an explanation of Curry-Howard isomorphism because I think that would not be very intuitive to many people because the most commonly used type systems have very little power to express logical properties about the program.

I may write another article about this.

Re: Where Do Type Systems Come From?

#138

Post by Animats » Sat, Jul 08, 2017, 7:22 PM UTC

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 people can run it again.)[2]

In Boyer-Moore theory, all functions are total - you can apply any function to any object. Types are predicates. Here's a definition of ORDERED for a list of number:

    (DEFN ORDERED (L)
      (IF (LISTP L)
          (IF (LISTP (CDR L))
              (IF (LESSP (CADR L)
                         (CAR L))
                  F
                  (ORDERED (CDR L)))
              T)
          T))

If L is not a list, it is considered to be ordered. This makes it a total function, runnable on any input, even though the result for the "wrong" type is not useful. This provides the benefits of types without requiring a theory of types. It's a very clean way to look at the foundations of mathematics. It's simpler than Russell and Whitehead.

When you prove things using definitions like this, there's a lot of case analysis. This gets worse combinatorially; a theorem with four variables with type constraints will generate at least 2⁴ cases, only one of which is interesting. Most of the cases, such as when L is not a list, are trivial, but have to be analyzed. Computers are great at this, and the Boyer-Moore prover deals with those cases without any trouble. But it went against a long tradition in mathematics of avoiding case analysis. That made this approach unpopular with the generation of pre-computer mathematicians. Today, it would be more acceptable.

(It's fun to run the Boyer-Moore prover today. In the 1980s, it took 45 minutes to grind through the basic theory of numbers. Now it takes a few seconds.)

[1] https://www.amazon.com/Computational-Logic-Robert-S-Boyer/dp... [2] https://github.com/John-Nagle/nqthm

Re: Where Do Type Systems Come From?

#139

Post by jcranberry » Sat, Jul 08, 2017, 7:25 PM UTC

agumonkey wrote: post #111

igravious wrote: post #39

Earlier quoted context omitted.

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 tha…

This was fantastically well stated.

Re: Where Do Type Systems Come From?

#140

Post by owebmaster » Sat, Jul 08, 2017, 7:31 PM UTC

incan1275 wrote: post #48

I share the author's frustration with wikipedia sometimes - people usually go to wikipedia for a distilled, comprehensible description of the subject matter. What he quoted was certainly not comprehensible, even to someone well-educated in CS foundations.

I like it because of it. If what I found in wikipedia was the "easiest" description, I'd find it lacking. It is better to not understand everything on the first read than understanding almost nothing because of lack of profoundity.