Types

https://gist.github.com/garybernhardt/122909856b570c5c457a6cd674795a9c?

by ivank • 10 years ago

445 192 10 years ago

gist.github.com

th0ma5• 10 years ago

Hope this makes it into Wikipedia instead of here.

paulddraper3• 10 years ago

It'll get moderated out.

NhanH5• 10 years ago

For this article specifically, it shouldn't be on wiki. The quality still needs a lot of polish, and too much opinions.

twblalock3• 10 years ago

The Idris example seems to need further explanation:

In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument":
add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat
add x y = x + y

That's all well and good, if you know the values of x and y at compile time. Consider a program that reads x and y from STDIN. The user could provide an x that is equal to or larger than y (or could provide only one value, or values that are not numbers). I see no way to deal with that except to throw a runtime error. Is that what would happen?

platz3• 10 years ago

not in idris, because it would force you to do that check manually and pass in the evidence as proof. it has a bunch of tools to help you do this.. namely lifting values into types with 'dependent pairs'. idris doesnt automagically calculate everything for you, but makes sure at compile time, that you provide evidence at run time for the things you have asserted in the types. it makes more sense after going through some of the tutorials and books.

NhanH5• 10 years ago

I do NOT know anything about Idris, but I'd imagine you have to do a check along the line of `if (x<y) then` before being able to call `add`, within that block-scope, the compiler should be able to infer that x<y. Typescript has something similar, where if you do `if (foo)`, the compiler will know that foo can't be null or undefined.

_ibu9• 10 years ago

The missing explanation is that `smaller` is a third argument to the function. It's type is a proof that x <= y. Since it is in curly brackets with the auto keyword, the compiler will fill in this proof in many cases, like when the values are statically known.

In the case where the values are read from the external environment, first you would have to compare them before calling the function. The comparator would return either a proof that x <= y, or x > y. In the first case you plug that value into the `smaller` argument, in the second case it's your responsibility to signal whatever kind of application-specific error is appropriate (assuming x > y is some kind of erroneous condition).

platz3• 10 years ago

though the comparator cannot return just a boolean, because it could be 'wrong'. this is where the dependent constructs come in to make sure the answer is correct

twblalock3• 10 years ago

What would happen if you did not compare them before calling the function, and just passed them in such that x >= y?

seanwilson12• 10 years ago

That's all well and good, if you know the values of x and y at compile time. Consider a program that reads x and y from STDIN. The user could provide an x that is equal to or larger than y (or could provide only one value, or values that are not numbers). I see no way to deal with that except to throw a runtime error. Is that what would happen?

Before you could call "add", you would have to add a branch/condition to verify "x" and "y" met the pre-conditions. The compiler would then know from the context of where you called "add" that the pre-conditions were always met. As you couldn't guarantee the pre-conditions were always met, you would have a code branch that decides what to do when the pre-conditions aren't satisfied.

The important difference to other languages though is that the compiler enforces that you're never allowed to call "add" unless you know the inputs satisfy the pre-conditions.

continuational2• 10 years ago

x = readFromStdin

y = readFromStdin

if(x < y) {

// in this scope, you have proven x < y

} else {

// in this scope, you have proven x >= y

}

doomrobo• 10 years ago

x and y do not have to be known at compile time. If I let y be a random Nat, and x be y - 1 (or 0 if y == 0), then I can statically prove that LE x y.

lanna• 10 years ago

To draw an analogy with more mainstream type systems, say you have a function like add(x: Int, y: Int): Int (takes two integers and returns an integer).

Now, somewhere else in your code, you have something like:

x = readline()

y = readline()

add(x, y)

That won't compile because readline returns string and add expects integers. Somewhere between readline and add you'll have to convert the strings to integers, and that piece of code (not the add function) is the one that has to be concerned with things like the user entering "abc" where a number is expected.

As far as the add function itself is concerned, it will always be invoked with two integers; the burden of proof is on the caller.

exDM69• 10 years ago

Consider a program that reads x and y from STDIN.

A program like this should fail to compile! You can't feed two arbitrary numbers from stdin to the "add" function above. In order to make it compile, you'd need to add some logic that uses min/max to swap the values so x is less than y.

lqdc13• 10 years ago

I think types can be both frustrating and life-saving.

However, the "danger" for me lies primarily in implicit conversion. That is, Python vs Lua/JS/R. When writing large programs, some things happen implicitly and linting may not catch it.

Everything else besides implicit conversion just helps structure the programs in specific ways and helps speed them up.

seanwilson12• 10 years ago

Great overview article but I have a comment.

In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument":
If we try to call this function as add 2 1, where the first argument is larger than the second, then the compiler will reject the program at compile time.
Haskell has no equivalent of the Idris type above, and Go has no equivalent of either the Idris type or the Haskell type. As a result, Idris can prevent many bugs that Haskell can't, and Haskell can prevent many bugs that Go can't. In both cases, we need additional type system features, which make the language more complex.

I really wish when people talk about dependently typed programming languages (e.g. Idris, Coq, Agda, ATS), they would mention the effort involved to get these compile time checks to happen.

These languages allow you to capture almost any program property you can think of as a type. Instead of being limited to saying function F "returns a number/list/string" like common type systems, you can capture arbitrarily complex properties like "F returns an even number", "F returns a permutation of the input list", "F always halts" or "F returns a proof of Fermat's Last Theorem". You don't get this for free and you have to help the computer verify these.

Proving F matches the type is arbitrary hard and is impossible to automated in general (e.g. the halting problem tells us we cannot always tell if a function halts). For example, consider the type "F returns a sorted permutation of the input list", where F could be an implementation of bubble sort, quicksort, merge sort, radix sort or something even more complex. Each algorithm will require a different and potentially complex proof and most of the time the programmer needs to help the computer find the proof. It's completely unlike what people are used to from type systems and is an even more massive leap than for someone moving from the type systems of e.g. C++/Java to Haskell.

I'm glad people are more aware of dependently typed languages but I feel the immense jump in how practical they are to use is severely overlooked.

continuational2• 10 years ago

To some degree, you can choose what you want to prove about your algorithms in those languages.

It's perfectly possible to implement a sorting algorithm without proving that it actually sorts the input, or indeed returns a permutation of the input list at all.

In that sense, you can choose how much efford you want to put into it.

seanwilson12• 10 years ago

To some degree, you can choose what you want to prove about your algorithms in those languages. It's perfectly possible to implement a sorting algorithm without proving that it actually sorts the input, or indeed returns a permutation of the input list at all.

Sure, but my point is that any nontrivial property requires the programmer to write difficult formal mathematical proofs which is an activity completely unlike what you see in mainstream strongly typed languages (e.g. Haskell, OCaml).

Also, consider how when you start making use of generics in type systems by converting all you Object lists to String lists; you find you have to start adding generic types all over the place for any code that touches that code until the compiler errors stop. If you decided to capture permutations of input lists in a dependently typed language, the exact same thing happens except this time capturing that property for all your algorithms could be monumental task of writing complex proofs (unlike before where you're just labelling things).

catnaroek28• 10 years ago

Agreed. These days, the most popular dependently typed languages are based on some variant of Martin-Löf type theory, in which arbitrary mathematical propositions are expressible at the type level. I'm not convinced that these designs offer a good power/cost ratio. For example, these languages often have very limited type inference.

In practice, most of the properties that a programmer (rather than, say, a mathematician using a proof assistant) would want to enforce mechanically (say, invariants of data structures) are expressible as first-order statements (lambda-bound variables are never applied). This strongly suggests that the ergonomics of dependent types could be significantly improved by deliberately limiting their expressive power. By the way, the idea isn't new: the Damas-Milner type system, which is most certainly known and proven technology, is a subset of System F-omega's type system for which type inference is possible, at the reasonable (IMO) price of not having higher-ranked or higher-kinded types. A dependently typed language with a first-order type level would benefit from reusing the basic architecture of a Damas-Milner type checker: a constraint generator and a constraint solver powered by a first-order unification engine.

seanwilson12• 10 years ago

By the way, the idea of deliberately limiting the expressive power of types isn't new: the Damas-Milner type system, which is most certainly known and proven technology, is a first-order subset of System F-omega's type system for which type inference is possible. A dependently typed language with a first-order type level would benefit from reusing the basic architecture of a Damas-Milner type checker: a constraint generator and a constraint solver powered by a first-order unification engine.

Have you seen languages like DML (let's you capture linear arithmetic properties only and automates the proof of these)?

https://www.cs.bu.edu/~hwxi/DML/DML.html

Dependent ML (DML) is a conservative extension of the functional programming language ML. The type system of DML enriches that of ML with a restricted form of dependent types. This allows many interesting program properties such as memory safety and termination to be captured in the type system of DML and then be verified at compiler-time.

What program properties are useful to capture and what properties you can mostly automate is a really interesting problem.

jroesch5• 10 years ago

Type inference isn't the most important, most languages that employ type inference are moving towards features sets make full inference hard, if not impossible. Not to mention you can get pretty good "inference" in dependently typed programming languages just by designing an appropriate higher order unification procedure. I have never met a daily user of these tools that find this to be the bottleneck.

In practice you spend way more time writing proofs in these system then doing anything else. There is evidence that we don't need to limit the expressive power of our logics, just design appropriate automation for the logic. Lean, a new ITT based theorem prover from MSR, has been focused on building automation for type theory. It already has promising results that formal methods techniques can be scaled to type theory (see the website for more information on recent work).

logicchains• 10 years ago

You don't get this for free and you have to help the computer verify these.

For library types, the most commonly used properties will have already been proven; you wouldn't have to write a proof that "sort" sorts a list any more than you'd have to write the sort function itself.

The computer can also be surprisingly good at proving these things in many cases. E.g. I was playing with the proof assistant Isabelle recently, and I tried to prove that given an int, a proof that twice that int is greater than 13, and a proof that four times that int is less than 29, then that int must be 7. I thought I'd have to fiddle around with induction on Peano numbers and the like, but nope, it could be proved with just a single "by arith".

catnaroek28• 10 years ago

it could be proved with just a single "by arith".

Tactics are probably a usability improvement for mathematicians who are used to proving everything by hand. But for programmers used to type inference, they're a step backwards. Mathematicians typically prove much deeper results, but they do so at a much slower rate than programmers write programs.

seanwilson12• 10 years ago

For library types, the most commonly used properties will have already been proven; you wouldn't have to write a proof that "sort" sorts a list any more than you'd have to write the sort function itself.

Sorting was just an example. Most proofs of nontrivial algorithms come with reams of hand written proofs. Happy to see examples that go against this though.

The computer can also be surprisingly good at proving these things in many cases. E.g. I was playing with the proof assistant Isabelle recently, and I tried to prove that given an int, a proof that twice that int is greater than 13, and a proof that four times that int is less than 29, then that int must be 7. I thought I'd have to fiddle around with induction on Peano numbers and the like, but nope, it could be proved with just a single "by arith".

Doesn't that just fall into the Presburger arithmetic decision procedure? The problem is you can rarely tell when the proof assistant is going to complete the proof for you (e.g. you're fine if it's within Presburger arithmetic but not if it requires induction).

tomp• 10 years ago

Proving F matches the type is arbitrary hard and is impossible to automated in general

So what?

Even proving that array indices are not accessed out of bounds within loops would be a considerable leap in the state of the art of industrial programming languages. For most cases (i.e. linear integer arithmetics), that's always automatically (dis-)provable. We have to start somewhere...

marcosdumay2• 10 years ago

The only time I remember using indexed list access in Haskell was on a dirty script that would break in 3 months anyhow. They are just ugly, and throw a huge amount of safety away, for no big gain at all.

Mainstream languages will gain much more from better iterators than by a ton of effort that just proves your indexes are within bounds.

seanwilson12• 10 years ago

Even proving that array indices are not accessed out of bounds within loops would be a considerable leap in the state of the art of industrial programming languages. For most cases (i.e. linear integer arithmetics), that's always automatically (dis-)provable. We have to start somewhere...

It's a super interesting and important area, I was just pointing out it was a challenging one with lots of open issues.

NhanH5• 10 years ago

The article is mainly focused on static typing. I guess it makes sense since the title is "Types". Although reading this, you might just think that dynamic typing is good for nothing.

The more practical part of the article is great. However, the theoretical part could use some works. Especially the terminology isn't actually clear.

Takes some example, what is "memory-safe" ? The only example makes it sounds like bound checking. And what does "no way to escape the language's type rules" mean? There are some usages of "valid program" and "invalid program" that makes my spider sense tingling as well.

However, no dynamic language can match the speed of carefully written static code in a language like Rust.
Any blanket statement of the form "static languages are better at x than dynamic languages" is almost certainly nonsense.

Those two quoted statements come from the article.

The section "Arguments for static and dynamic types" didn't mention a single reason why dynamic typing could be preferable over static-typing. It could at least have mentioned macro, or hand-waving claim that dynamic typing makes for prettier code at time (I think the author of python's requests library made that argument in one of the blog post).

I think the last part should be removed (ranking the language by their typed system power).

There's a clear trend toward more powerful systems over time, especially when judging by language popularity rather than languages simply existing.

Well, it looks true since we didn't consider any dynamic language at all...

Focusing more on the "Concrete examples of type system power differences" would have been better for the article, I think. Something along the line of an example of Non-nullable type with something simple in TS, to optional/maybe monad, then dependent type that you can implement matrix multiplication (m * n) with (n * p) and got the type (m * p) back.

epidemian• 10 years ago

The author is highly probably on the static typing camp.

First and foremost, i don't think dividing people into these clear-cut "camps" is good for this discussion (and probably for most discussions too...).

Second, i very much doubt that the author is a purist of static typing, or even a strong proponent of it. He has a series of programming screencasts called Destroy All Software, and in most the episodes i've seen he uses Ruby, Bash or Python. So, unless he has dramatically changed his style since then, i don't think he has any problems using dynamically typed languages.

NhanH5• 10 years ago

Sure, I will edit that sentence out.

hawski• 10 years ago

> However, no dynamic language can match the speed of carefully written static code in a language like Rust.
> Any blanket statement of the form "static languages are better at x than dynamic languages" is almost certainly nonsense.
Those two quoted statements come from the article.

I think author had in mind "ALL static languages are better at x than ALL dynamic languages" as a nonsense. He probably didn't have in mind that "A static language_ IS better at x than A dynamic language_" is a nonsense.

AnimalMuppet4• 10 years ago

And what does "no way to escape the language's type rules" mean?

I can give you an example, from bitter experience.

In the original Pascal, the size of an array was part of the type of an array. There was no possible type for a variable-sized array. And you couldn't cast from an array of one fixed size to an array of another fixed size.

Well, we were trying to do a 2D numerical simulation on a grid, with the size of the grid being user-specified. The original version of the program used a linked list to simulate the array, since you could have an arbitrarily-long linked list. But this meant that, if the simulation was 60x60, to reference the cell directly below the current one, you had to follow 60 links to get there!

I replaced it with a 2D array of a fixed size, with the size being the largest amount we could fit into available memory (it was on an embedded system, so the amount of memory available was predictable). Of that, we used only the user-specified subset to do the simulation.

TL;DR: If you need to do something that's outside what's allowed by your type system, and there's no way to escape the language's type system, you're trapped.

junke2• 10 years ago

    1 + eval(read_from_the_network())

> If we get an integer, that expression is fine; if we get a string, it's not. We can't know what we'll get until we actually run, so we can't statically analyze the type.

The unsatisfying solution used in practice is to give eval() the type Any, which is like Object in some OO languages or interface {} in Go: it's the type that can have any value. Values of type Any aren't constrained in any way, so this effectively removes the type system's ability to help us with code involving eval. Languages with both eval and a type system have to abandon type safety whenever eval is used.

No, you can give EVAL a returning type of any (T) but still make type inference work.

    (+ 1 (eval (read)))

The meaning of a type in SBCL is: if an expression evaluates without error, then its type is .... In other words, the type of the above expression is NUMBER.

There is also a NIL type (bottom) which represent the empty set of values. If a function has a return type of NIL, it means that it does not return a value normally. This is the case for the ERROR function, or the (LOOP) expression.

evincarofautumn• 10 years ago

if an expression evaluates without error, then its type is…

What’s curious is that this is true in every language with general recursion/looping:

    int f(int n) {
        while (true) {}
        return n + 1;
    }

(In other words, the type of “f” isn’t the logical formula “a → a”, but rather “a → ¬¬a”.)

The type of “eval” can also be fully static; it can just return a type that you have to do case analysis or runtime type inspection on to use.

In Haskell, with a data type:

    data Value = Integer Int | Text String | ...

    eval :: String -> Value

    foo = do
      value <- read_from_the_network
      let result = eval value
      case result of
        Integer n -> return (1 + n)
        _ -> error "that was not an integer!"

Or with RTTI:

    eval :: String -> Dynamic

    foo = do
      value <- read_from_the_network
      let result = eval value
      case fromDynamic result of
        Just n -> return (1 + n)
        Nothing -> error "that was not an integer!"

“fromDynamic” has the type:

    Typeable a => Dynamic -> Maybe a

Which is to say “given a dynamic value, and its runtime type information, I can either give you the value back with a static type, or nothing if I can’t perform the downcast”—much like “dynamic_cast” on pointer types in C++.

junke2• 10 years ago

What’s curious is that this is true in every language with general recursion/looping:

Yes, thanks for pointing that out.

The type of “eval” can also be fully static; it can just return a type that you have to do case analysis or runtime type inspection on to use.

I'd say that's what type T stands for in Lisp, since you can then dynamically dispatch on the actual type of the value.

mietek3• 10 years ago

The type of “eval” can also be fully static; it can just return a type that you have to do case analysis or runtime type inspection on to use.

Yes! The problem is, we don’t have a static type system which would allow us to intensionally analyse syntax at runtime. See section 9 of Sheard (2001) “Accomplishments and research challenges in meta-programming”.

https://www.dropbox.com/s/pathrmr7rufkw1d/Sheard2001.pdf

If you’re interested in this subject, perhaps drop in to #dependent on Freenode IRC, or ping me on Twitter.

titanomachy3• 10 years ago

Someone who has experience with both Agda and Idris, could you comment on which is easier to get started with? Coming from a Haskell background, I'd like to try my hand at writing more interesting constraints into my types. Any experiences using these languages for (non-research) work?

I've played around with Coq a little and it certainly feels more like a proof assistant than a programming language. It was fairly confusing and unfamiliar, but interesting nonetheless. Something with slightly more traditional ergonomics might be easier to pick up.

seanwilson12• 10 years ago

Someone who has experience with both Agda and Idris, could you comment on which is easier to get started with? Coming from a Haskell background, I'd like to try my hand at writing more interesting constraints into my types. Any experiences using these languages for (non-research) work?

The learning curve is almost vertical to be completely honest from personal experience. I find most tutorials are written by people with a strong background in logic, type systems and mathematics, so it's a struggle to rely only on your knowledge of mainstream programming languages as you're learning lots of new things at once (e.g. formal proofs, formal specifications, logic, pure functional programming).

It's a super interesting area if you can stick with it though so keep at it!

titanomachy3• 10 years ago

most tutorials are written by people with a strong background in logic, type systems, and mathematics...

I'm a little used to this from Haskell, although I imagine the dependently-typed languages are even worse in that regard. Working through the Idris tutorial now and at least the syntax is familiar.

lmm7• 10 years ago

I have very limited experience, but it's worth saying that Idris was designed by an experienced Haskell user with the intention of using it to write practical programs.

bjz_3• 10 years ago

I found Idris pretty easy to get started with - that's part of it's goal, making dependent types easier to get started with. From there I think it would be easier to go to Agda or Coq, but I haven't explored much there myself.

whateveracct• 10 years ago

+1 for Idris. The tutorials were pretty solid for it too when I tried it, and the mailing list was very helpful when I had questions [1]. There's even a WIP book! [2]

[1] https://groups.google.com/forum/#!forum/idris-lang

[2] https://www.manning.com/books/type-driven-development-with-i...

titanomachy3• 10 years ago

Thanks. I've started with the tutorials but have yet to see an example that convinces me it's worth all the pain. I'll carry on a little further, though.

EDIT: the pain of such a strict language, not necessarily idris in particular.

DSMan1952762• 10 years ago

Being someone who enjoys C (Though I readily admit the type system is generally weak compared to the others on the list) there's a little misinformation on this page that I think it worth clearing up - though I think the majority of the information is still perfectly good:

C does not 'allow' you to do a lot of the things mentioned on this page, it just doesn't generally carry around all the information to check and make sure you don't. So the page is generally still right - it can be fairly easy to get memory-unsafe things past the compiler - though whether you want to blame the type-system or blame the compiler could be debated, probably a bit of both.

Reading past the ends of arrays is illegal, as is accessing a variable of one type through a pointer to another type. Some of these things will get checked or assumed by the compiler (And thus break code that does these things, and in some ways break them in subtle ways), but there's no guarantee that the compiler actually knows you broke the rules. This tends to be the main different from other languages like Java, where the compiler/run-time does carry around such information and thus can do such checks and does know you when you broke the rules.

With that said, while there are some things I don't like about the design of Rust overall, giving the compiler more information to be able to figure out the above is definitely one thing they did right in comparison to C. The problem C is approaching is that, even though compilers are getting smarter, enough code was already written before that was the case to result in breaking when you attempt to use 'smarter' compilers.

naasking19• 10 years ago

Since this articles is about types, any behaviour the compiler doesn't check or doesn't generate a type error is "allowed".

DSMan1952762• 10 years ago

The issue with that idea is that there is more than one C compiler. Some of them issue no warnings at all, and some of them (like `gcc`) will yell at you and probably break your code if you attempt to do some of the things I outlined.

I disagree with saying it is 'allowed' by the type system, because a smart C compiler could throw out your code and refuse to compile it if you do such things, and in doing so would still be within the C standard. Some work has already been done on this front in `gcc` (And I would assume `clang`) - the issue tends to be that by doing this, you end-up breaking some older code that used to work fine. And since older compilers didn't enforce these rules, people aren't as aware of them.

wz1000• 10 years ago

    add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat
    add x y = x + y

Actually, (GHC) Haskell can express something like this type if you turn on the required extensions.

    data Nat = Z | S Z deriving (Eq, Ord, Show)
    data SNat (n :: Nat) where
        SZ :: SNat Z
        SS :: SNat n -> SNat (S n)

    type family Compare (a :: Nat) (b :: Nat) :: Ordering where
      Compare Z Z = EQ
      Compare (S a) Z = GT
      Compare Z (S a) = LT
      Compare (S a) (S b) = Compare a b
    
    type a < b = Compare a b ~ LT

    type family (+) (a :: Nat) (b :: Nat) :: Nat where
      Z + a = a
      a + Z = a
      (S a) + b = S (a + b)
    
    add :: (a < b) => SNat a -> SNat b -> SNat (a+b)
    add = ...

DanWaterworth4• 10 years ago

Haskell has no equivalent of the Idris type above, and Go has no equivalent of either the Idris type or the Haskell type. As a result, Idris can prevent many bugs that Haskell can't, and Haskell can prevent many bugs that Go can't. In both cases, we need additional type system features, which make the language more complex.

Type checking Idris is much simpler than Haskell.

gary_bernhardt5• 10 years ago

It doesn't say "type checking", though. It says "the language", which I think of as including the respective preludes.

jroesch5• 10 years ago

The core theory (and implementation) is much simpler for almost all dependent type theories. At least this is my personal feeling after having read a lot of GHC code, written an Idris backend, the native backend for Lean, and significant portions of `rustc`.

tome• 10 years ago

Type checking Idris is much simpler than Haskell.

Is it? How's that?

DanWaterworth4• 10 years ago

Haskell's type system has accrued complexity over the years, whereas a small dependently typed language can be implemented very easily [1].

[1] https://www.andres-loeh.de/LambdaPi/

jroesch5• 10 years ago

A short answer is that the theory is just simpler. Non-dependent type theory spends a lot of effort separating values, types, kinds and valid operations over them. For example you need lots of extensions to make it possible to use a type both at the value, type, and kind level in Haskell. Each extension to the type system adds more complexity, and requires special code to implement its functionality (DataKinds, PolyKinds, TypeFamilies, etc). You also end up needing at least two or more different kinds of ASTs one that describes expressions, one for types, one for kinds, etc.

All of this falls away in dependent type theory you can represent the whole language with a class of pesudo-terms. For example the core expressions can be captured by the below grammar:

    term := x
         | f x
         | forall (x : Type), B x
         | lambda (x : A), e
         | Type

Type checking (not inference) is straight forward to implement for these theories and can be done in about a page or two of code. Of course "elaboration" or "type-inference" for these theories can be much more complex, but Haskell's isn't simple either. The most recent publication on the TI algorithm is roughly 80 pages.

kpmah• 10 years ago

I wrote a little article, which has been posted here before, that shows the power of different type systems and what kind of bugs you can expect to prevent: http://kevinmahoney.co.uk/articles/tests-vs-types/

arianvanp2• 10 years ago

If we try to call this function as add 2 1, where the first argument is larger than the second, then the compiler will reject the program at compile time

This is not entirely true in general. auto is only a best bet. It might not be able to prove something right and will fail. For example, if it has to recurse deeper than 100 constructors. In this case, the user of the function has to provide a proof himself.

See it as a bloom filter. if it doesn't fail, you're sure your function is correctly called. if it does fail, it might still be correctly called but the compiler just didn't have enough time to prove it. In that case a user needs to convince the compiler that he is right.

gary_bernhardt5• 10 years ago

I don't see the problem here. I said that Idris will reject the program if the proof fails. That's what you're saying too, unless I'm very confused. (It's late, so maybe I am?)

arianvanp2• 10 years ago

Yes, but it might also reject correct programs. that's the point I'm trying to make.

ozy4• 10 years ago

So what might make dynamic languages easier to write in? I enjoy dynamic languages more because:

* "double kilometerToMiles(double km) { return km / 1.6 }" here the types are of really low value, yet I have to type them in.

* a mutable list of generic and variable arity event handlers. Really hard to specify as a type (most languages cannot do it). Really easy to use.

* co- and contravariance and lists, the math works exactly opposite of intuition.

* when you change your mind on the types/arity beyond what your IDE can follow, it is a lot of low value work

* if your test suite has 100% coverage of arguments/return-value and field usage, you have type checked your program.

If I am going to write down types, they better be of value to me. Like types that are null or non-null, or tainted (from the user) or non-tainted. Or two numbers that are kilometers vs miles. Or only accessible under a certain lock or other preconditions. And be flow sensitive (kotlin style null checks), not make me write even more code.

But if you are a dynamic language, do be strong typed (no "1" == 1). Also be dynamic in arity, that is (part-of) a type. Don't be handwavy scoped, lexical scoping is probably the only predictable way to do scoping. Fail fast, like prevent spelling mistakes for non existing field names for example. And allow this to work: "2 * Vector(10,10)".

And from that perspective there is still quite some room for improvement in all classes of languages, I suppose, and good that there is lot of movement and experiments today.

lucian1900• 10 years ago

Writing down the types isn't a necessary property of static type systems. In Haskell, F# or (OCa)ML, you almost never have to actually mention any types.

I do agree that Java-style types aren't of much value. That catches few errors at significant cost.

MrBuddyCasino• 10 years ago

Catching logical errors is only one out of several things that static typing gives you.

Incidentally, right now this is a few positions above this posting: https://news.ycombinator.com/item?id=12350063

Better IDE support, a kind of self-documentation and increased performance come to mind. I know there are counter-examples for each of these points, but the general trend cannot be denied.

paulddraper3• 10 years ago

The cost of non-Java-style types is compile time :)

lmm7• 10 years ago

* "double kilometerToMiles(double km) { return km / 1.6 }" here the types are of really low value, yet I have to type them in.

You shouldn't have to, and you wouldn't in say Haskell.

a mutable list of generic and variable arity event handlers. Really hard to specify as a type (most languages cannot do it). Really easy to use.

You want the handlers to have types corresponding to the events they handle, right? I.e. a labelled product/coproduct (similar to HList). They do exist.

* co- and contravariance and lists, the math works exactly opposite of intuition.

I don't understand the claim here?

* when you change your mind on the types/arity beyond what your IDE can follow, it is a lot of low value work

In a well-designed language most of your functions will be generic, and the parts you have to change should only be the parts that your change actually affects. Obv. this ideal is not fully achieved yet, but we keep getting better at it.

* if your test suite has 100% coverage of arguments/return-value and field usage, you have type checked your program.

Not true. That one example works for a given function does not prove the type is correct for all arguments. As a trivial example you could define a function like "def f(i) = if(i == 1000) "blah" else i". Typechecking would catch that immediately, but to catch it through testing you'd have to test every possible integer as input.

ozy4• 10 years ago

To most commenters: Indeed static typing has advantages as well, I just didn't list them. And some languages solve certain "complaints" I had.

I would suggest though, that comparing haskell to javascript, is almost like comparing a train with an offroad bike. Which you choose when is a discussion at a whole different level.

As for the list of event handlers example. The point it is a trivial piece of code. Any jQuery plugin writer can do it. Yet the type math behind it is complex. Java cannot express it. Most languages cannot be generic in function arity so cannot express it. Spending time on it is not worth the trouble. And paying this penalty at API level, where ever user has to pay, is just a sin.

Some discussion from the dartlang on covariant lists: https://www.dartlang.org/articles/design-decisions/why-dart-...

The test suite idea was incorrect. Even 100% code coverage will not do. But for "normal" code, add reasonable amount of coverage. And any production runtime type error will be really surprising. And even when it does happen, the fix is clear and quick.

A personal feeling on this topic is that it is all tradeoffs. But it makes me really happy to see gradual typing gaining traction. So you can start on your offroad bike, but end on a well oiled train, where that is worth the tradeoff. So you don't have to choose up front. Perhaps when we can even get runtime guarantees on perf/object layout when the type checker is happy.

kilotaras• 10 years ago

double kilometerToMiles(double km) { return km / 1.6 }

But what if you could have `miles kilometersToMiles(kilometers km)`? Under the hood its the same old doubles but you would be able to catch errors such as the one that caused Surveyor failure [1].

e.g. Haskell has units[2] and dimensional[3] that allow you to do exactly that

[1] https://en.wikipedia.org/wiki/Mars_Climate_Orbiter#Cause_of_...

[2] https://github.com/goldfirere/units

[3] https://github.com/bjornbm/dimensional

spriggan3• 10 years ago

* if your test suite has 100% coverage of arguments/return-value and field usage, you have type checked your program.

The most horrible argument in favor dynamic typing in my opinion. Test suits shouldn't be about checking if a return value is of expected type, that's ridiculous. It's implementing a type checker manually.

There are a lot of things statically typed languages can do to make types painless :

- (global) type inference (Crystal does that)

- co and contravariance, it is not limited to dynamically typed language

- optional parameters

- adhoc type declaration like in C# (ex {x:1,y:"a"} is a type).

- contracts

- pattern matching

- generics

- ect ... etc ...

I just dislike dynamically typed languages. Even interpreted languages should be statically typed IMHO. Again, there are multiple ways to make statically typed language painless when it comes to types.

ozy4• 10 years ago

Test suits shouldn't be about checking if a return value is of expected type

Indeed and so they don't have to. When you have reasonable code coverage, it is really surprising to encounter type issues in production. And they are the easiest mistakes to fix. But the point is, runtime checks happen implicitly as you run the code. So no "implementing a type checker" needed ...

On the other hand my comment on when you get the equivalent of being fully type checked was incorrect. Even 100% code coverage will not guarantee it for some code.

I like both kind of languages, and use both. While you get some advantages in static languages, you do also pay a price in language semantics and effort. It is good to point that out, so we can continue making progress, like Crystal or latest C# (and latest F#!). There used to be a time when the mood was: Java is good for all, stop confusing us with your new languages.

naasking19• 10 years ago

* if your test suite has 100% coverage of arguments/return-value and field usage, you have type checked your program.

This is absolutely false. Others have pointed this out, but types are much more general than runtime checks in dynamically typed languages. For instance, you can check at compile-time that your program doesn't have data races or deadlocks:

http://www-kb.is.s.u-tokyo.ac.jp/~koba/typical/

Or design a library in Haskell to ensure file handles and other scarce resources are promptly reclaimed:

http://okmij.org/ftp/Haskell/regions.html#light-weight

Neither of these are testable in dynamically typed languages. Static types are much more powerful than dynamic types, in general.

marcosdumay2• 10 years ago

"double kilometerToMiles(double km) { return km / 1.6 }"

What about:

  toMiles (Kilometers k) = Miles (k/1.6)

Then you do:

  let x = Kilometers 5
  print (toMiles x)

And, of course, any calculation will only accept the correct units. At this naive implementation, you'll have to add the conversions to satisfy the compiler, but there are Haskell libraries that bring automatic conversions too.

Anyway:

Like types that are null or non-null, or tainted (from the user) or non-tainted.

That's Haskell.

Or two numbers that are kilometers vs miles.

That's my example up there.

Or only accessible under a certain lock or other preconditions.

Yep, Haskell.

And be flow sensitive (kotlin style null checks), not make me write even more code.

That's emulating what people do in Haskell.

one-more-minute2• 10 years ago

If this topic interests you, Julia's type system is worth checking out [1]. Julia is unusual among dynamic languages not just for having a powerful type system (including parametric types), but also for making it idiomatic to make full use of types. Aside from the benefits to the programmer, this also allows the compiler to get to Rust-level performance where it's needed.

I find that this is a nice compromise that gets a lot of the benefits of static type systems (small, local errors as opposed to behavioural bugs, ability to express concepts and constraints) without the drawbacks (loss of interactivity, or inability to escape the type system when it's appropriate).

[1] http://docs.julialang.org/en/latest/manual/types/

lmm7• 10 years ago

It sounds very ad-hoc? (And Julia's benchmarking has not been reputable in the past, FWIW).

without the drawbacks (loss of interactivity, or inability to escape the type system when it's appropriate).

One can absolutely have interactivity in a statically typed language, and virtually all statically typed languages support casting when you absolutely need to.

one-more-minute2• 10 years ago

"Ad-hoc" seems subjective but to me it feels very carefully thought out. And while I've found the benchmarks to be accurate, I more importantly mean myself (and many others I know) being easily able to get high performance code when we need it.

My second paragraph was only a personal take on what works for me, so YMMV, but nevertheless: I'm not arguing against static type systems in principle, but these are practical concerns rather than theoretical ones. I don't know of a mainstream static language that supports a fully dynamic REPL (Haskell's isn't great) and casting back and forth to `interface{}`, `Object`, or `Any` everywhere is a huge overhead compared to duck typing. I look forward to a future language solving those issues, but that's not the case today.

amelius• 10 years ago

A type is a collection of possible values

Ok, but do two collections with the same values always correspond to the same type?

paulddraper3• 10 years ago

Yes, but if remember you can always say that the values are different.

A blue 5, and a red 5.

Five feet, or five inches.

munificent• 10 years ago

Yes, they do.

kd0amg• 10 years ago

It depends on the language. If you have, for example, a type-and-effect system, a type can contain information (like "we wrote to stdout while computing this") that is never reflected in the value itself. In a formal setting, it's more appropriate to describe a type as a collection of pieces of source code, so that `2+3` and `print "computing...\n"; 2+3` have different types even though they'll evaluate to the same thing.

acjohnson552• 10 years ago

Generally, no, at least with nominal typing.

naasking19• 10 years ago

Decent overview of many concepts, but the opening line isn't strictly true:

A type is a collection of possible values.

A type is a proposition, and "This binding has one of these possible values" is merely one type of proposition. So a type is much more powerful than a simple set-based interpretation, even though this is how most people think about it.

For instance, in Haskell you can encode a region calculus that ensures prompt reclamation of file handles and other scarce resources [1]. The relations between nested regions to ensure correctness seems awkward to interpret as a set, but it's straightforward if you just think of types as a relation.

[1] http://okmij.org/ftp/Haskell/regions.html#light-weight

chriswarbo3• 10 years ago

Well, there are several ways to think about types, especially regarding this article, which tries to cover static and dynamic types.

Most formal definitions/treatments of types I've come across do not apply to dynamic types at all; usually the typing formalism says nothing about dynamically typed programs/values other than giving them one big recursive type. What we would informally call "dynamic types" are then treated completely separately, e.g. via "tags".

While such distinctions are certainly useful, an introductory/broad-overview explanation like this seems to benefit without such complications/distractions.

naasking19• 10 years ago

While such distinctions are certainly useful, an introductory/broad-overview explanation like this seems to benefit without such complications/distractions.

I don't think misrepresenting types is the way to go. An introduction like I just gave seems simple enough, where a type is a proposition about a program, and you just then explain that most such propositions are "variable X may take on values from set Y".

It's important not to perpetuate the false notion that sets of simple sets of values suffice to explain types, because it entails the common and equally false notion that full test coverage in a dynamically typed language suffices to match the safety of a statically typed language.

rntz• 10 years ago

(Static) types may be seen as propositions, but this is just one interpretation of them. We can also interpret types as sets (although this doesn't work out very well except in very simple languages), as domains (most commonly), as cpos, as relations over closed terms (PERs), and so forth.

The types-as-propositions interpretation is a particularly useful one because it lets us take ideas from the field of formal logic and apply them to programming. But it is only one interpretation, and not a definition of what types are.

I don't think it's possible to give "type" a good, short definition. For me John Reynolds' definition comes closest: "Type structure is a syntactic discipline for enforcing levels of abstraction." But that's rather a mouthful, and not a good introduction to what types are.

A type is a proposition, and "This binding has one of these possible values" is merely one type of proposition.

The type that an expression or variable has does not correspond to the proposition that that expression has a certain set of possible values! You're mixing the object-level (the language & its types) with the meta-level (assertions about the language). This is a total misunderstanding of Curry-Howard. Rather, the values an expression might take on can be interpreted as proofs of the corresponding proposition.

naasking19• 10 years ago

(Static) types may be seen as propositions, but this is just one interpretation of them. We can also interpret types as sets (although this doesn't work out very well except in very simple languages), as domains (most commonly), as cpos, as relations over closed terms (PERs), and so forth.

Right, I wasn't advancing the propositional definition as the only one, merely as one that sufficiently captures the generality, because the article's current definition of types-as-sets is insufficiently general.

catnaroek28• 10 years ago

For me John Reynolds' definition comes closest: "Type structure is a syntactic discipline for enforcing levels of abstraction." But that's rather a mouthful, and not a good introduction to what types are.

The nice thing about this definition is that it reveals why reflection renders a type system useless: it destroys the type system's ability to enforce abstractions.

eli_gottlieb4• 10 years ago

The types-as-propositions interpretation is a particularly useful one because it lets us take ideas from the field of formal logic and apply them to programming. But it is only one interpretation, and not a definition of what types are.

Ehhh, it kind of is a definition. Think of it this way: a type system is a topology we lay over programs, with open sets representing observable (using finite computation) properties and closed sets representing deniable (using finite computation) properties. The finest such topology possible is the Scott topology, which can distinguish every single observable value and deniable property from every other: it encodes all the information you can have about a program without solving the Halting Problem.

Type systems, then, are coarser topologies over programs than that one, which group observably different expressions and traces into the same open sets, which are then called "types". When those types are guaranteed not to contain _|_, the divergent program, they can also be considered topological spaces, with the programs in them acting as points in the topological space.

dllthomas• 10 years ago

merely one type of proposition

Shouldn't that read "one kind of proposition"?

acjohnson552• 10 years ago

Formalism aside, it seems like it's most useful in practice to think of type as defining what can be done with a value. The sidesteps the idea of type being something permanent and inherent to a value. In practice, the type might be metadata discoverable and actionable at run-time, it might be something that exists at compile-time to determine correctness of a program (based on how values are used), or both.

Does this point of view leave out anything crucial?

naasking19• 10 years ago

Formalism aside, it seems like it's most useful in practice to think of type as defining what can be done with a value.

That might be a simpler way of explaining it, since "proposition" is rather abstract. Or perhaps, a type defines the valid state transitions your program can undergo at any given point, ie. given the data in your program (the program state S0), the types of all of that data define a set of valid transitions to another data set (program state S1).

levbrie2• 10 years ago

Kind of shocked nobody mentioned this, even if it is a bit of an aside, but umm, I've been dying for anything at all from Gary Bernhardt - I don't even know what to say except that it makes me hope however unrealistically that will one day get something like the magnum opus that is "Destroy All Software" from him again.

dochtman• 10 years ago

You know he just started to post new stuff, right?

https://www.destroyallsoftware.com/screencasts/catalog

levbrie2• 10 years ago

I know. Mind blown.

nickpsecurity4• 10 years ago

I havent read/seen it. Im guessing you know more than Id see in an abstract. So, what's the significance of that work?

athenot• 10 years ago

I've been very curious about Perl6's gradual typing[1] which, as I understand it, draws a lot from Haskell's type system but in an optional manner.

    subset NonNegativeInt of Int where * >= 0;
    
    sub fib(NonNegativeInt $nth) {
      given $nth {
        when 0  { 0 }
        when 1  { 1 }
        default { fib($nth-1) + fib($nth-2) }
      }
    }

[1] http://blogs.perl.org/users/ovid/2015/02/avoid-a-common-soft...

zeveb• 10 years ago

The unsatisfying solution used in practice is to give eval() the type Any, which is like Object in some OO languages or interface {} in Go: it's the type that can have any value. Values of type Any aren't constrained in any way, so this effectively removes the type system's ability to help us with code involving eval. Languages with both eval and a type system have to abandon type safety whenever eval is used.

It's not quite true that they must abandon type safety: rather, they must abandon a certain kind of compile-time type check. It's not unsafe to use eval or Any values (i.e., it won't crash the system); one must simply examine the Any value (at runtime, natch) and do stuff with it.

eximius• 10 years ago

So, how do these advanced types work?

For their `add` example, I imagine just having x<y somewhere is sufficient. But let's say I write a sorting implementation but the compiler can't quite figure out that it is correct. Is there a provided way to tell the compiler 'trust me, this property is now true'?

Also, I'm assuming the compiler has two classes of errors here: a counter example vs. unable to prove?

Can anyone point me to documentation on these (in Idris, preferably)?

icen2• 10 years ago

In Idris, there are functions `believe_me` and `really_believe_me`, which assert things to the compiler. They're generally only used for FFI code, or for extremely tedious proofs.

If you wanted to prove that a list was sorted, you'd write another datatype:

    IsSorted : Ord a => List a -> Type

which represents the proposition that the input list is sorted. You could encode this by requiring that any new element in the list is either the first element, or less than or equal to the previous element. Then, your sorting function could return a dependent pair:

    (l : List a ** IsSorted l)

which can be read as the list, accompanied by a proof that it is, in fact, sorted. Since your `IsSorted` type requires that the list is sorted, via construction, you won't be able to supply the output of the function unless your code is correct (or you use `believe_me`!).

The compiler doesn't generally come up with counterexamples for you; with this style, if the proof isn't complete, it won't compile.

mamcx• 10 years ago

I read that type checking is easier with dependent types.

I'm barely aware of adga adn other langs that are used for profs, but wonder how useful (and what danger ahead) could cause to design a language with this for more mundane purposes (like, for example, build websites, data manipulation, gui, etc)

rpazyaquian• 10 years ago

What types are and what they do is all well and good, but what I want to know is how they would help me write a larger application. Would it help it be more correct, be written faster, or be more flexible? Does it just help on a line-by-line programming basis, or can it have any ramifications on a higher level like product design?

Types

Related Stories