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

Types

gist.github.com

Post reply on HN
Print view View original

41–50 of 198 posts

Re: Types

#41

Post by seanwilson »

logicchains wrote: post #34
seanwilson wrote: post #11

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

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

> 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).

Re: Types

#42

Post by kazagistar »

twblalock wrote: post #28
seanwilson wrote: post #17

Earlier quoted context omitted.

> What would happen if you did not compare them before calling the function, and just passed them in such that x >= y? It would be a type error. All the compiler would know is that "x" and "y" are strings/integers so it would tell you they were the wrong type. If you do a branch on checking they are the correct type, then in that part of the branch the compiler will know they are the correct type and allow "add" to b…

Assuming they were integers before, what type would they become after they were compared?

Its not that they change type. Its that the comparison function returns either a proof that one is greater then the other, or that they are equal. When you are in the right branch, you can pass that proof (type) along with the value into other functions.

Re: Types

#43

Post by gary_bernhardt »

DanWaterworth wrote: post #38

> 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.

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

Re: Types

#44

Post by jroesch »

catnaroek wrote: post #22
seanwilson wrote: post #11

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

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

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).

Re: Types

#45

Post by tome »

DanWaterworth wrote: post #38

> 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.

> Type checking Idris is much simpler than Haskell.

Is it? How's that?

Re: Types

#46

Post by catnaroek »

jroesch wrote: post #39
seanwilson wrote: post #32

Earlier quoted context omitted.

Any examples? I'm curious for examples of a nontrivial type that would catch lots of common programming errors where the proofs can be automated. I see lots of new dependently typed languages but not much interest in addressing the proof automation aspect.

You don't need type theory to verify program properties, people have been using first-order methods for decades to prove properties about programs. For example there was a line of work in ACL2 that verified a microprocessor implementation, as well as plenty of modern work using tools like SMT to automatically prove program properties, see Dafny, F* for language based approaches. Though there is plenty of language agn…

Nice. SMT can be (and indeed has been) integrated into type-based approaches to program verification as well.

Re: Types

#47

Post by junke »

evincarofautumn wrote: post #40
junke wrote: post #20

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

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

> 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.

Re: Types

#48

Post by jroesch »

gary_bernhardt wrote: post #43
DanWaterworth wrote: post #38

> 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.

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

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`.

Re: Types

#49

Post by DanWaterworth »

tome wrote: post #45
DanWaterworth wrote: post #38

> 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.

> Type checking Idris is much simpler than Haskell. Is it? How's that?

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/

Post reply on HN