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

51–60 of 198 posts

Re: Types

#51

Post by catnaroek »

jroesch wrote: post #44
catnaroek wrote: post #22

Earlier quoted context omitted.

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

> Type inference isn't important, most languages that employ type inference are moving towards features sets make full inference hard, if not impossible.

What I'm saying is that I don't like this direction, because type inference is very important to me.

> Not to mention you can get pretty good "inference" in dependently typed programming languages just by designing an appropriate higher order unification procedure.

Such higher-order unification procedures must always be tailored towards specific use cases, since higher-order unification is in general undecidable. Effectively implementing a different type checking algorithm for every program I write doesn't feel like good use of my time.

What I want is a type system that is more honest about how much it can help me: it only promises to enforce properties expressible as first-order statements, but offers much better inference, and the remainder of my proof obligation is hopefully small enough that I can fulfill it manually.

> In practice you spend way more time writing proofs in these system then doing anything else.

Indeed, and that's what I'd like to fix.

Re: Types

#52

Post by gary_bernhardt »

NhanH wrote: post #10
paulddraper wrote: post #9

Earlier quoted context omitted.

It'll get moderated out.

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

This is a decent summary of why I'm doing it. Wikipedia is full of "high quality" content, where "high quality" means "directly exposing every detail that anyone ever thought to nitpick", and this topic is a nitpicker's paradise. There's value in that detail-heavy style, but it's difficult to learn from and it's a type of writing that I rarely want to read. As for opinions (and lack thereof), they prevent Wikipedia from saying many things that are both well-known and easily stated. The lack of clear summaries of widespread disagreeing opinions keeps our implicit knowledge implicit.

Re: Types

#53

Post by NhanH »

gary_bernhardt wrote: post #52
NhanH wrote: post #10

Earlier quoted context omitted.

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

This is a decent summary of why I'm doing it. Wikipedia is full of "high quality" content, where "high quality" means "directly exposing every detail that anyone ever thought to nitpick", and this topic is a nitpicker's paradise. There's value in that detail-heavy style, but it's difficult to learn from and it's a type of writing that I rarely want to read. As for opinions (and lack thereof), they prevent Wikipedia f…

I agree with your reasoning and your description of Wikipedia.

However, despite all the flaws, wiki is reasonably helpful, and I doubt filling it with more opinions would be helping the case.

Re: Types

#54

Post by jroesch »

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?

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.

Re: Types

#55

Post by arianvanp »

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

Re: Types

#56

Post by jroesch »

catnaroek wrote: post #46
jroesch wrote: post #39

Earlier quoted context omitted.

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.

Yeah I think SMT is really the state-of-the-art right now in this area. Leo De Moura (one of the main authors of Z3) has been working on Lean for the past couple of years. There is a small group of us (5~) who have been working on a big release for the past couple of months. The goal is to bring the easy of use of SMT automation to type theory, so you can get both the ability to do induction and automation.

Lean: http://leanprover.github.io/

Re: Types

#57

Post by gary_bernhardt »

jroesch wrote: post #48
gary_bernhardt wrote: post #43

Earlier quoted context omitted.

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

It's generally (or maybe universally) more difficult to "get" dependent typing than plain old ML-family static typing. I mean, this HN comments page alone has multiple threads where people don't think that the "x > y" proof example even works. For most programmers, that's how non-obvious the possibility of proving nontrivial properties of code is. Maybe I should change the wording in the OP to make it clear that I'm talking about the set of ideas required to use the language, not the characters that need to be typed into a computer to make it work.

Re: Types

#58

Post by Ericson2314 »

catnaroek wrote: post #35
logicchains wrote: post #34

Earlier quoted context omitted.

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

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

Huh tactics are pretty great. Say exactly what you want and the computer programs itself!

It's unfair to just compare development time between tactic-generated programs in a dependent language with manually written programs in a non-depenendent language. The end result in the dependent language is much more valuable.

Re: Types

#59

Post by platz »

kazagistar wrote: post #42
twblalock wrote: post #28

Earlier quoted context omitted.

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.

here's a full code example:

    import Data.String

    -- takes two integers, and a proof that x  
      (y : Integer) -> 
      (prf : x      -- require a proof that that x  print (add x y prf)
        No => putStrLn "no prf, x is not less than y"
lets say I mess up the sign of the comparison on the case line and write decEq (x > y) instead... then I'd get a type error

    When checking argument prf to function Main.add:
    Type mismatch between
                x > y = True (Type of prf)
        and
                x
there's no way to construct the prf value artificially, or sneak in different parameters that are unrelated to the prf value.

it's either a compile error or it's valid.

Re: Types

#60

Post by gary_bernhardt »

arianvanp wrote: post #55

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

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?)
Post reply on HN