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

Dependent Haskell

serokell.io

Post reply on HN
Print view View original

71–80 of 92 posts

Re: Dependent Haskell

#71

Post by tom_mellior »

tomp wrote: post #44

I fundamentally disagree with the author's thesis. I don't think dependent types are the future of development, but instead I'd bet on refined types (or contracts - see my experiment [0], Liquid Haskell [1] by Ranjit Jhala, and languages Dafny [2] and F* [3] developed by Microsoft on top of Z3 SMT theorem prover [4]), where constraints are explicit yet simple, and proven automatically by an automated theorem prover.…

> I don't think dependent types are the future of development, but instead I'd bet on refined types

> ...

> lookup : (a : array) -> (n : int if 0 whatever

https://en.wikipedia.org/wiki/Dependent_type: "In computer science and logic, a dependent type is a type whose definition depends on a value."

In your example, you are using a dependent type: The type of n depends on the value a. So your refined types are dependent types, but possibly restricted in some way. Can you explain the restrictions you have in mind to clarify (and motivate) the relationship between full dependent types and your refined ones? Is it something purely syntactic like "linear arithmetic only" (as I believe was the case for Liquid Types, at least originally) to ensure decidability?

Edit: Even the very first sentence of the very first paper about Liquid Types (the base of Liquid Haskell) talks about dependent types: "We present Logically Qualified Data Types, abbreviated to Liquid Types, a system [...] to automatically infer dependent types precise enough to prove a variety of safety properties." (emphasis mine)

Re: Dependent Haskell

#72

Post by newen »

jlokier wrote: post #51
lmm wrote: post #39

Earlier quoted context omitted.

If you want to engage productively, remember that people tend to say things they think are true, so look for a way to read it that makes sense rather than going out of your way to find a way to read it that makes it false. (I guess nitpicking the phrasing for a "middlebrow dismissal" is the best way to get upvotes here nowadays). > nothing about this list implies "runs fast." It doesn't imply it, but it enables it; r…

> > The implication is that memory-safe languages do not have memory leaks, which is completely false. > There's no such implication, only that memory-unsafety leads to memory leaks, which is true. If we're going to read in the spirit of "looking for a way to read things that make sense rather than going out of your way to find a way to read it that makes it false"... Then it depends which sort of implication. https:…

Not really. p therefore q implies not p therefore not q is a very basic logical fallacy. Making a statement does not imply it's inverse.

Re: Dependent Haskell

#73

Post by torben-friis »

empath75 wrote: post #55
torben-friis wrote: post #42

Earlier quoted context omitted.

I'd argue that the informative value is pretty much zero: If a programmer is familiar with lambda calculus, lazy languages, and algebraic types, then there's just no way that person isn't also somewhat familiar with haskell. The explanation is gibberish for those who need it, so its only use is to be self congratulatory for those who don't.

This point of view is alien to me. Why, when you see words you don’t understand, don’t you make an effort to learn what they mean? How on earth did you ever become a coder with this kind of attitude?

I do understand them, I'm into functional programming and I've toyed with haskell in the past. I'm just aware that such a definition makes it sound more daunting than it really is, mostly because of that "just".

It's kinda like the running joke of "a monad is a monoid in the category of endofunctors, what's so hard about it?", but said in a non-sarcastical manner.

Re: Dependent Haskell

#74

Post by tomp »

tom_mellior wrote: post #71
tomp wrote: post #44

I fundamentally disagree with the author's thesis. I don't think dependent types are the future of development, but instead I'd bet on refined types (or contracts - see my experiment [0], Liquid Haskell [1] by Ranjit Jhala, and languages Dafny [2] and F* [3] developed by Microsoft on top of Z3 SMT theorem prover [4]), where constraints are explicit yet simple, and proven automatically by an automated theorem prover.…

> I don't think dependent types are the future of development, but instead I'd bet on refined types > ... > lookup : (a : array) -> (n : int if 0 whatever https://en.wikipedia.org/wiki/Dependent_type : "In computer science and logic, a dependent type is a type whose definition depends on a value." In your example, you are using a dependent type: The type of n depends on the value a. So your refined types are dependen…

Right, the difference is to some degree syntactic, but then, so is most programming ("it's just math").

The most significant difference, as it appears to me (note that I've done only a bit of research into refined types, and practically none into dependent types), is that dependent types means building top-down whereas refined types means building bottom-up.

Dependent types: everything is proved, by hand, by the user, who has to build up the whole program from basic blocks. Usually the "foundation" is taken to be some kind of type theory, either Martin-Löf Type Theory or more recently Homotopy Type Theory, which has some complexities (e.g. multiple types of equality) and limitations (e.g. languages cannot be Turing complete) that I don't really understand. "Pi types" abound. I'm not sure how much of this description really is fundamental about Type Theory, and how much is just due to the specifics of the implementations I've seen (Coq, Agda, Idris).

Refined types: start with a program and add some assertions about the values (and possibly functions, but this can then get more complicated) in the program. The idea is that many of these can ideally be proven by automated SMT solvers, which support some "theories" (e.g. natural numbers, real numbers, bitfields (i.e. machine integers and floating point numbers), algebraic datatypes) and can prove some statements in these theories. As you mentioned, "linear arithmetics", along with "real number algebra", are complete and decidable theories, so in theory you should be able to prove anything about them, but I'm guessing that in practice you'd still want some timeout parameter on your SMT solver (like in type systems, where there are exponential edge cases, that thankfully don't arise often in practice), but they aren't very useful, so hopefully you can prove more than that, using the heuristics embedded into SMT solvers (e.g. you should be able to prove many non-linear properties of two-dimensional loops by lifting integers into reals). If the solver is unable to solve something, the programmer can still add hints (but this quickly gets complicated).

A concrete difference would be, in dependently-typed language, you define a list type as

  type List a n =
    | Nil : List 'a 0
    | Const : a -> List a n -> List a (n + 1)
in a language with refined types, you can add length afterwards:

  type List a = 
  property length : List a -> Nat
And then the type checker/SMT solver will treat `length` as an uninterpreted function that always maps the same array to the same integer, and use it to prove things.

Not sure if this makes a lot of sense, I haven't looked into this in a while and am also not aware of the most recent research in these fields. Hopefully someone can explain better!

Re: Dependent Haskell

#75

Post by mietek »

tomp wrote: post #74
tom_mellior wrote: post #71

Earlier quoted context omitted.

> I don't think dependent types are the future of development, but instead I'd bet on refined types > ... > lookup : (a : array) -> (n : int if 0 whatever https://en.wikipedia.org/wiki/Dependent_type : "In computer science and logic, a dependent type is a type whose definition depends on a value." In your example, you are using a dependent type: The type of n depends on the value a. So your refined types are dependen…

Right, the difference is to some degree syntactic, but then, so is most programming ("it's just math"). The most significant difference, as it appears to me (note that I've done only a bit of research into refined types, and practically none into dependent types), is that dependent types means building top-down whereas refined types means building bottom-up. Dependent types: everything is proved, by hand, by the user…

> Usually the "foundation" is taken to be some kind of type theory … which has some … limitations (e.g. languages cannot be Turing complete) that I don't really understand …

One sentence summary that glosses over a lot of things:

In a dependently typed language, types can contain programs, and we want typechecking to terminate.

You may also want to read how the author of Idris explains partial and total functions:

https://livebook.manning.com/#!/book/type-driven-development...

Re: Dependent Haskell

#76

Post by coldtea »

lmm wrote: post #57
tomp wrote: post #54

Earlier quoted context omitted.

Maybe, but I think that's mostly an implementation issue... Not only will automated theorem provers get better, but the point is, they don't even need to prove anything! A program would be just as valid if you inserted runtime checks for all contracts, or just the ones you can't prove or disprove. Compare that to type systems, different languages have different ways of dealing with issues (e.g. you can disable type e…

> the point is, they don't even need to prove anything! A program would be just as valid if you inserted runtime checks for all contracts, or just the ones you can't prove or disprove. "Valid" in what sense? I want my code to refuse to compile when it's broken, not compile and then fail at runtime. I certainly don't want similar-looking checks to be usually compile time but occasionally runtime when things get compli…

>Sounds like gradual typing, which I've found a nightmare to work with in practice - all the pain but very little of the gain.

1) How is "gradual typing" any worse than (at worst case) dynamic typing? And even more so "a nightmare"?

2) What's the big pain ("all the pain") in static strong typing?

3) How is catching 95% of type issues "very little of the gain" of catching 100% of them?

Re: Dependent Haskell

#77

Post by lmm »

coldtea wrote: post #76
lmm wrote: post #57

Earlier quoted context omitted.

> the point is, they don't even need to prove anything! A program would be just as valid if you inserted runtime checks for all contracts, or just the ones you can't prove or disprove. "Valid" in what sense? I want my code to refuse to compile when it's broken, not compile and then fail at runtime. I certainly don't want similar-looking checks to be usually compile time but occasionally runtime when things get compli…

> Sounds like gradual typing, which I've found a nightmare to work with in practice - all the pain but very little of the gain. 1) How is "gradual typing" any worse than (at worst case) dynamic typing? And even more so "a nightmare"? 2) What's the big pain ("all the pain") in static strong typing? 3) How is catching 95% of type issues "very little of the gain" of catching 100% of them?

> 1) How is "gradual typing" any worse than (at worst case) dynamic typing? And even more so "a nightmare"?

Type declarations that are sometimes wrong can be misleading enough that I find code with them harder to work on than code with no types at all, personally.

> 2) What's the big pain ("all the pain") in static strong typing?

It's not a huge pain, but adding and maintaining types does have a cost (particularly when tooling support is limited).

> 3) How is catching 95% of type issues "very little of the gain" of catching 100% of them?

Because you can't trust the types to be correct in any given piece of code. You end up having to do all the things you would have to do in an untyped languge (high test coverage, carefully rechecking all the types when debugging issues, etc.).

Re: Dependent Haskell

#78

Post by mietek »

incadenza wrote: post #6

Does anybody care to explain dependent types? I’ve heard the term used in FP conversations but not sure I get it.

Two sentence summary that glosses over a lot of things:

1. Types can be used to classify programs.

2. Dependent types can be used to classify programs by running other programs on them.

If you would like to learn more about dependent types, ‘The Little Typer’ is newly out and a lot of fun to read:

https://mitpress.mit.edu/books/little-typer

Re: Dependent Haskell

#79

Post by tomp »

lmm wrote: post #77
coldtea wrote: post #76

Earlier quoted context omitted.

> Sounds like gradual typing, which I've found a nightmare to work with in practice - all the pain but very little of the gain. 1) How is "gradual typing" any worse than (at worst case) dynamic typing? And even more so "a nightmare"? 2) What's the big pain ("all the pain") in static strong typing? 3) How is catching 95% of type issues "very little of the gain" of catching 100% of them?

> 1) How is "gradual typing" any worse than (at worst case) dynamic typing? And even more so "a nightmare"? Type declarations that are sometimes wrong can be misleading enough that I find code with them harder to work on than code with no types at all, personally. > 2) What's the big pain ("all the pain") in static strong typing? It's not a huge pain, but adding and maintaining types does have a cost (particularly wh…

> that are sometimes wrong

That's not gradual typing, just the most common implementation of gradual typing (e.g. in Dart, TypeScript, Python, but not e.g. in Clojure and Perl 6 AFAIK). Although maybe this is just a "no true Scotsman" argument...

Re: Dependent Haskell

#80

Post by tom_mellior »

tomp wrote: post #74
tom_mellior wrote: post #71

Earlier quoted context omitted.

> I don't think dependent types are the future of development, but instead I'd bet on refined types > ... > lookup : (a : array) -> (n : int if 0 whatever https://en.wikipedia.org/wiki/Dependent_type : "In computer science and logic, a dependent type is a type whose definition depends on a value." In your example, you are using a dependent type: The type of n depends on the value a. So your refined types are dependen…

Right, the difference is to some degree syntactic, but then, so is most programming ("it's just math"). The most significant difference, as it appears to me (note that I've done only a bit of research into refined types, and practically none into dependent types), is that dependent types means building top-down whereas refined types means building bottom-up. Dependent types: everything is proved, by hand, by the user…

OK, I think I see where you're coming from. I don't think the distinction you make is a useful one.

> A concrete difference would be, in dependently-typed language, you define a list type as [...]

Coq is a dependently typed language, and while it has a definition like this for some thing (called vector, maybe? I forget), the definition for lists in the standard library is not dependent, and length is a separate function. You can still write a function like

    Fixpoint lookup (xs: list a) (idx: {n: nat | n
I don't know how much experience you have with dependently typed languages, but it looks like you might have misunderstood tutorials showing that one can define a dependent list type as saying that one must define lists dependently?

> And then the type checker/SMT solver will treat `length` as an uninterpreted function that always maps the same array to the same integer, and use it to prove things.

Treating it as uninterpreted is quite weak. It allows you to prove simple callers of the lookup function, but not the implementation. Also, you would not be able to prove something like this:

    if idx
This is admittedly a silly example, but it should be provable. But you can only do that if you can reason about the relationship between length and Cons.

As for automating proofs, I very very much agree that we need a lot more automation. But if that means crippling our theories to an extend that they are no longer expressive enough to verify our software, not much is won.

Post reply on HN