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

91–100 of 198 posts

Re: Types

#91

Post by harveywi »

catnaroek wrote: post #62
Ericson2314 wrote: post #58

Earlier quoted context omitted.

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.

I'm not comparing dependent types vs. no dependent types. I'm comparing higher-order dependent types (Agda, Idris, Coq, etc.) vs. first-order dependent types: https://news.ycombinator.com/item?id=12350147 Seriously, Coq-style proof scripts are utterly unredable when they grow past a certain size. The only way to understand them is to replay them, so that you can see the intermediate hypotheses and goals.

> The only way to understand them is to replay them

Reminds me of the same kind of problem that arises in trying to understand the runtime behavior of nontrivial programs involving side-effects, mutable state, multithreading, etc. Sometimes the debugger is the only practical way to figure out what the program is doing. Add concurrency into the mix, and things can get tricky very quickly.

Dependently-typed programming and machine-assisted proof is still an emerging thing, and there is probably lots of room for exploring ergonomic improvements. It will be interesting to see where this goes.

Re: Types

#92

Post by levbrie »

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.

Re: Types

#93

Post by dochtman »

levbrie wrote: post #92

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.

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

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

Re: Types

#94

Post by [deleted] »

dochtman wrote: post #93
levbrie wrote: post #92

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.

You know he just started to post new stuff, right? https://www.destroyallsoftware.com/screencasts/catalog

[deleted]

Re: Types

#95

Post by athenot »

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

Re: Types

#96

Post by lanna »

twblalock wrote: post #3

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

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.

Re: Types

#97

Post by catnaroek »

naasking wrote: post #88
catnaroek wrote: post #33

Earlier quoted context omitted.

I'd love to give more concrete examples, but I'm slightly hampered by the fact the type system I want isn't actually implemented anywhere. I have a rough sketch of the design of the type system I want, and I've been looking for a computer scientist, logician or mathematician to help me polish the design and prove that it is, in fact, type safe. But I couldn't find anyone. :-|

Why not just learn Coq or Agda yourself? There are also sorts of introductions for simple type systems that I'm sure you can build off of.

I have no idea how to implement fresh unification variable generation (my type system is a superset of Damas-Milner, kind of like how the calculus of constructions is a superset of System F-omega) in Coq or Agda. Everywhere I've seen it implemented, it involves mutable state. So, “in principle”, I could fake it using something like the state monad, and plumbing around the collection of unification variables generated so far, but in practice reasoning about this seems like a pain.

Re: Types

#98

Post by chriswarbo »

naasking wrote: post #87

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…

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.

Re: Types

#99

Post by catnaroek »

harveywi wrote: post #91
catnaroek wrote: post #62

Earlier quoted context omitted.

I'm not comparing dependent types vs. no dependent types. I'm comparing higher-order dependent types (Agda, Idris, Coq, etc.) vs. first-order dependent types: https://news.ycombinator.com/item?id=12350147 Seriously, Coq-style proof scripts are utterly unredable when they grow past a certain size. The only way to understand them is to replay them, so that you can see the intermediate hypotheses and goals.

> The only way to understand them is to replay them Reminds me of the same kind of problem that arises in trying to understand the runtime behavior of nontrivial programs involving side-effects, mutable state, multithreading, etc. Sometimes the debugger is the only practical way to figure out what the program is doing. Add concurrency into the mix, and things can get tricky very quickly. Dependently-typed programming…

Your analogy between debugging effectful programs and replaying proof scripts is frighteningly accurate.

Re: Types

#100

Post by exDM69 »

twblalock wrote: post #3

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

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

Post reply on HN