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

151–160 of 198 posts

Re: Types

#151

Post by marcosdumay »

ozy wrote: post #69

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

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

Re: Types

#152

Post by naasking »

catnaroek wrote: post #149
naasking wrote: post #148

Earlier quoted context omitted.

Hmm, I don't think you're being very charitable. That these programmers can write working programs suggest they sufficiently understand disjunction, conjunction, negation, conditionals and quantification. Perhaps they have trouble abstracting the semantics from their preferred language and/or syntax, but that doesn't mean they don't grasp their meaning.

I offer this thread as evidence: https://news.ycombinator.com/item?id=12342583

That's definitely not being charitable. Subtyping has some pretty subtle interaction with other typing features, which is why it's still being studied more than 20 years after Cardelli's "Subtyping Recursive Types".

The pernicious conflation of subtyping and subclassing in common OO programming languages just compounds the confusion.

Re: Types

#153

Post by nickpsecurity »

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.

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

Re: Types

#154

Post by nickpsecurity »

catnaroek wrote: post #147
nickpsecurity wrote: post #142

Earlier quoted context omitted.

I like your proposal of first-order, dependent types. Shocked I havent heard of it before now given advantages. I hope someone helps you build it. On related note, what do you think about the Shen LISP approach where Sequent Calculus can be used for advanced typing? Does it have the expressibility and decidability benefits you described? Hadn't seen many specialists talk about it so still an unknown to me. If it does…

I'm not familiar with Shen, but, if I recall correctly, its type system is Turing-complete, so it's probably more complicated than I'd be comfortable with. IMO, the topmost priority in a type system designed for programmers ought to be automation, not expressiveness. Programmers don't spend their time proving deep theorems. Most of what a programmer does is actually fairly boring, but it ought to be done correctly, r…

I totally agree. They're not going to use it if we make them work for it. Neither work hard or even lightly. Needs to be no harder than basic annotations but preferably closer to existing, static typing. Let them focus on functions instead of proofs.

Re: Types

#155

Post by imh »

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.

That's mostly true, but the speed programmers write programs depends how bulletproof they have to be. There have been times that if you include the debugging and maintainability difficulty, proving things to my compiler would be a step forward for me. There's probably a sweet spot.

Re: Types

#156

Post by jackmott »

platz wrote: post #59
kazagistar wrote: post #42

Earlier quoted context omitted.

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…

that is pretty awesome

Re: Types

#157

Post by catnaroek »

imh wrote: post #155
catnaroek wrote: post #35

Earlier quoted context omitted.

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

That's mostly true, but the speed programmers write programs depends how bulletproof they have to be. There have been times that if you include the debugging and maintainability difficulty, proving things to my compiler would be a step forward for me. There's probably a sweet spot.

> That's mostly true, but the speed programmers write programs depends how bulletproof they have to be.

Of course, but, in any case, writing programs at the same rate mathematicians prove theorems simply isn't viable.

Re: Types

#158

Post by dllthomas »

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…

> merely one type of proposition

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

:p

Re: Types

#159

Post by eli_gottlieb »

rntz wrote: post #118
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…

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

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

Re: Types

#160

Post by seanwilson »

thinkpad20 wrote: post #107
seanwilson wrote: post #41

Earlier quoted context omitted.

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

You don't have to write a proof if you don't want to. It's quite possible to simply write your sorting function without a proof, it's just that at that point you don't know that your function works as advertised (which of course is then just the same thing that you get in a non-dependently-typed language). data Comp = Gt | Lt | Eq sortBy : (a -> a -> Comp) -> List a -> List a sortBy = ... The above is perfectly accep…

> You don't have to write a proof if you don't want to.

I know this, I'm simply pointing out that when you do decide to write a proof it can be a very challenging task (much harder than adding generic types into Java code for example).

Post reply on HN