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

191–198 of 198 posts

Re: Types

#191

Post by catnaroek »

dragonwriter wrote: post #188
catnaroek wrote: post #187

Earlier quoted context omitted.

> The most obvious is that it makes intent explicit in the case of multiple similarity Keep in mind that similarity is explicitly intended to be a quick-n-dirty form of code reuse. If the programmer has enough time to refactor the code, he or she should probably factor out the common parts, and then use proper (subtyping) inheritance. In view of this, I don't think making similarity overly complicated is a good idea.…

> If the programmer has enough time to refactor the code, he or she should probably factor out the common parts, and then use proper (subtyping) inheritance. I do see the attraction of the idea that all implementation sharing ultimately reflects something that can be expressed through a subtyping hierarchy adhering to the LSP, but I'm not 100% convinced that it is the case. Absent certainty on that point, I'd like to…

> I agree that static verification of sanity in subtyping inheritance reduces the problem of LSP violations

The LSP itself is never violated in a type-safe language. What's violated is the guarantees that you expected the LSP to buy you. For instance, Java doesn't promise about the meaning of non-final methods. If a programmer assumes such guarantees, the problem is with the programmer, not Java. If he wants such guarantees to hold, he has to use a different language.

Re: Types

#192

Post by catnaroek »

naasking wrote: post #190
catnaroek wrote: post #179

Earlier quoted context omitted.

(0) I didn't say all types. I said datatypes. (1) Induction on datatypes is a powerful tool for reasoning about programs in strict languages, and it's only possible when you regard datatypes as collections of values.

Then data types are a restricted notion of types for which induction applies, so we agree that types in general are not a collection of values.

All types in a call-by-value language are two collections: one of values and another of expressions, the former embeddable in the latter. This is plain obvious when you see its operational semantics.

Re: Types

#193

Post by titanomachy »

bjz_ wrote: post #85
titanomachy wrote: post #23

Someone who has experience with both Agda and Idris, could you comment on which is easier to get started with? Coming from a Haskell background, I'd like to try my hand at writing more interesting constraints into my types. Any experiences using these languages for (non-research) work? I've played around with Coq a little and it certainly feels more like a proof assistant than a programming language. It was fairly co…

I found Idris pretty easy to get started with - that's part of it's goal, making dependent types easier to get started with. From there I think it would be easier to go to Agda or Coq, but I haven't explored much there myself.

Thanks. I've started with the tutorials but have yet to see an example that convinces me it's worth all the pain. I'll carry on a little further, though.

EDIT: the pain of such a strict language, not necessarily idris in particular.

Re: Types

#194

Post by eli_gottlieb »

catnaroek wrote: post #182
dragonwriter wrote: post #180

Earlier quoted context omitted.

If classes are types, subsclasses should be subtypes -- so the above restrictions should just be applied to subclass relationships. One could also have an non-subclassing mechanism of implementation sharing, that might be declared something like this: class Related does (method1, method2) like Base; or class Related does all except (method3) like Base;

That syntax is too heavyweight (IMO). AFAICT, most of the time, when people use inheritance, they don't want to define perfect subtypes. They just want to reuse as much already implemented behavior as possible.

Very true. Mixin delegation is the thing we actually want here.

Re: Types

#195

Post by tel »

catnaroek wrote: post #168
tel wrote: post #164

Earlier quoted context omitted.

I disagree that it's a good idea to think of types as a "collection" (loosely) of values. It may be the case that you do not distinguish computation and value (here, I'm thinking of CBPV) but types only classify values as interpreted via their embedding into expressions.

If a type couldn't be regarded as a collection of values in a strict language, then induction on datatypes would simply be unsound. Of course, induction on datatypes is unsound in Haskell, but it's sound in Standard ML.

Not all types need to have induction principles. The ones that do are nicer, of course, precisely because they correspond to values.

Re: Types

#196

Post by matej_kosik »

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.

I had/have a similar feeling.

I have thought about it some time ago and came up with the following proposal:

http://matej-kosik.github.io/www/doc/coq/coq-trunk-proof-tre...

Re: Types

#197

Post by ozy »

lmm wrote: post #169
ozy wrote: post #114

Earlier quoted context omitted.

To most commenters: Indeed static typing has advantages as well, I just didn't list them. And some languages solve certain "complaints" I had. I would suggest though, that comparing haskell to javascript, is almost like comparing a train with an offroad bike. Which you choose when is a discussion at a whole different level. As for the list of event handlers example. The point it is a trivial piece of code. Any jQuery…

> The point it is a trivial piece of code. Any jQuery plugin writer can do it. Yet the type math behind it is complex. Java cannot express it. Most languages cannot be generic in function arity so cannot express it. As the quote goes, dynamic typing is the belief that you can't explain to a computer why your code works, but you can keep track of it all in your head. If it's really hard to express in a given language…

I only see this now. Good reply. All valid concerns. But

> "I want all runtime errors to be at least this surprising", that level will be easier to achieve via types than via tests

For the type of the values, yes, but you still need tests for the content of the values. E.g you can only index into arrays with integers, but can your code access the array out of bounds? So that level is implicitly achieved.

> but the trouble is that code that's 95% typechecked might as well be 0% typechecked

That is absolutely not my experience. Typed at module boundaries really helps, even is that is only 5% of the code. On the other hand, getting to 100% type checked can be hard in current gradual systems. Mostly because some code is hard to type, even though it works fine, and humans can reason about it fine. Though you might be right, it is probably better expressed in a more type sound way. (Unless it is parametrization on function arity that does you in, grr.)

But to me, unless you are coding in idris or such, types are like the derivative of your code. Yes they show the general "slope"; how it fits together. But it says nothing on the values that flow through it, or the correctness of the code. You still need tests, and the type checker is not much more than a spell checker. Its usefulness is not in dispute (though overestimated by some). Just that in most of todays popular languages, you pay a price that is not non trivial. The choice is a tradeoff.

Re: Types

#198

Post by lmm »

ozy wrote: post #197
lmm wrote: post #169

Earlier quoted context omitted.

> The point it is a trivial piece of code. Any jQuery plugin writer can do it. Yet the type math behind it is complex. Java cannot express it. Most languages cannot be generic in function arity so cannot express it. As the quote goes, dynamic typing is the belief that you can't explain to a computer why your code works, but you can keep track of it all in your head. If it's really hard to express in a given language…

I only see this now. Good reply. All valid concerns. But > "I want all runtime errors to be at least this surprising", that level will be easier to achieve via types than via tests For the type of the values, yes, but you still need tests for the content of the values. E.g you can only index into arrays with integers, but can your code access the array out of bounds? So that level is implicitly achieved. > but the tr…

> For the type of the values, yes, but you still need tests for the content of the values. E.g you can only index into arrays with integers, but can your code access the array out of bounds? So that level is implicitly achieved.

So you create a path-dependent type for valid indices into a given array (or, more likely, use a safe way of expressing iteration so that you don't need to see indices directly). Yes you can check that your indexing is valid with tests, but it's more efficient to do it with types.

> That is absolutely not my experience. Typed at module boundaries really helps, even is that is only 5% of the code.

Maybe if they're enforced at those boundaries - does that happen? I'm thinking mainly of gradual typecheckers that are erased at runtime, which IME are useless, because a type error can easily propagate a long way before it's actually picked up, and you see an "impossible" error where something has a different type at runtime to its declared type.

> But to me, unless you are coding in idris or such, types are like the derivative of your code. Yes they show the general "slope"; how it fits together. But it says nothing on the values that flow through it, or the correctness of the code.

Not my experience once you get used to working with the type system. Anything that should always be true in a given part of the code, you make into part of the types. Make the types detailed enough that a function with a given signature can only have one possible meaning, and then any implementation of that function that typechecks must be correct.

Post reply on HN