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

Programming paradigms that change how you think about coding

brikis98.blogspot.com

Post reply on HN
Print view View original

81–90 of 206 posts

Re: Programming paradigms that change how you think about coding

#81

Post by quandrum »

jarrett wrote: post #63

A thought on dependent types: Can a dependent type system catch all type errors at compile time? For example, suppose I write the following (in pseudo-code): // Variable x is an integer greater than or equal to 0 and less than 256. int x (>=0, I can imagine how a compiler could catch that kind of error. But that's trivial. What happens in programs like this: int x (>= 0, Now the compiler can't know for sure whether t…

Yes

  int x (>= 0,
Dependent Type systems don't have to know what is possible keyboard input. They have to know what type the getKeyboardType function returns (and the parseInt), and if it's possible for that type to be out of the range of your constraint.

If that's so, it throws an error. At that point you simply have to compose your types and functions so they match the constraint, and you know you are safe.

Re: Programming paradigms that change how you think about coding

#82

Post by wging »

vilhelm_s wrote: post #79
tel wrote: post #68

Earlier quoted context omitted.

Your idea about `maybe (int (>= 0, In a DT language when you express such a type the compiler will demand that you write a type like maybe which can fail at runtime and demand that you handle that failure. To the compiler, `int` and `int (>= 0, To you final point about tracking constraints, even those defined implicitly, I think the answer is no-ish. Most frequently, DT languages have such a richness of types that th…

Agreed in general, but it is possible to enable this style of constraint propagation by being restrictive about what kind of contraints you can write. In particular, the "LIQUID" family of languanges that have been developed at UCSD allows properties which are conjunctions of LInear IneQUlites, and can infer them automatically. The programmer would annotate one declaration of a variable with a constraint like (0 Thei…

http://goto.ucsd.edu:8090/index.html ?

Re: Programming paradigms that change how you think about coding

#83

Post by jarrett »

quandrum wrote: post #81
jarrett wrote: post #63

A thought on dependent types: Can a dependent type system catch all type errors at compile time? For example, suppose I write the following (in pseudo-code): // Variable x is an integer greater than or equal to 0 and less than 256. int x (>=0, I can imagine how a compiler could catch that kind of error. But that's trivial. What happens in programs like this: int x (>= 0, Now the compiler can't know for sure whether t…

Yes int x (>= 0, Dependent Type systems don't have to know what is possible keyboard input. They have to know what type the getKeyboardType function returns (and the parseInt), and if it's possible for that type to be out of the range of your constraint. If that's so, it throws an error. At that point you simply have to compose your types and functions so they match the constraint, and you know you are safe.

> if it's possible for that type to be out of the range of your constraint....If that's so, it throws an error.

If I'm understanding you correctly, that would seem to take a lot of the power out of dependent type systems. Almost all values will eventually depend on input from the outside world, so it seems you'd rarely have a chance to use your dependent type system.

Haskell (which doesn't have dependent types baked in) has a good approach to possibly-invalid data via the Maybe type. E.g. Maybe Int means "either an integer, or nothing." So it forces you to explicitly handle the possible error cases.[1]

To spell it out in Haskell terms: In the example of getting an integer from the keyboard, x is a Maybe Int. If the input is invalid, the value is set to Nothing, which is a unique constant. If it's valid, the value is of type Just Int.

> At that point you simply have to compose your types and functions so they match the constraint, and you know you are safe.

But how do you get from untrusted, potentially invalid data into the world of trusted, guaranteed-valid data? How do you bridge the gap? I was suggesting some combination of an applyConstraint function and a Maybe type to achieve that. Are there other ways?

[1] Actually, it will let you bypass the usual compile-time protections with the fromJust function. But if you want compile-time safety, either refrain from using fromJust, or use it only where you're absolutely sure the value won't be Nothing.

Re: Programming paradigms that change how you think about coding

#84

Post by abecedarius »

protomyth wrote: post #80

I've been thinking a lot about agent-oriented programming. I had a General Magic device back in the day and later thought the concept of a Telescript like language as applied more for code organization than code mobility might be interesting. I guess APIs won, but I still think there is something there.

http://erights.org/ was not technically like Telescript, but aimed at a similar-enough vision you might find it interesting. http://erights.org/elib/capability/ode/index.html for that vision. The section on mobile almost-code at http://erights.org/elib/distrib/pipeline.html should help to relate it to Telescript.

Re: Programming paradigms that change how you think about coding

#85

Post by Xophmeister »

copx wrote: post #48
Xophmeister wrote: post #27

Earlier quoted context omitted.

The second paragraph: > This is not your grandma's "functional programming will change the world!" blog post Presumably because a lot of people write blog posts about how FP will change your approach. That's true but, while I wouldn't say FP is mainstream, it's well-known in circles such as ours; whereas the topics he mentions are much less run-of-the-mill. It makes for a more interesting and original read. I notice…

I think your perception of what is "well-known" strongly depends on your age. For example neither concatenative nor declarative programming are exotic to me and I think many other older programmers. Forth (concatenative) used to be pretty big, back then software was simpler and you did not need a Qt wrapper, XML parser etc. Forth was very practical for the things it was originally used for. Like that embedded control…

Good point. To be honest, I was somewhat surprised to see 'declarative programming' in the list, as well, given the ubiquity of SQL and regular expressions; plus, as others have said, FP's declarative nature.

Re: Programming paradigms that change how you think about coding

#86

Post by randyrand »

jarrett wrote: post #63

A thought on dependent types: Can a dependent type system catch all type errors at compile time? For example, suppose I write the following (in pseudo-code): // Variable x is an integer greater than or equal to 0 and less than 256. int x (>=0, I can imagine how a compiler could catch that kind of error. But that's trivial. What happens in programs like this: int x (>= 0, Now the compiler can't know for sure whether t…

| int x (>= 0, Will be a compile time error because getKeyBoard input returns integers that are between 0-256(?) not 0-10 like 'x' wants.

Re: Programming paradigms that change how you think about coding

#87

Post by jarrett »

dllthomas wrote: post #75
jarrett wrote: post #63

A thought on dependent types: Can a dependent type system catch all type errors at compile time? For example, suppose I write the following (in pseudo-code): // Variable x is an integer greater than or equal to 0 and less than 256. int x (>=0, I can imagine how a compiler could catch that kind of error. But that's trivial. What happens in programs like this: int x (>= 0, Now the compiler can't know for sure whether t…

"Can a dependent type system catch all type errors at compile time?" Provably not, if you want a type checker guaranteed to finish.

Could you give a brief overview of why? Does this come down to the halting problem?

Re: Programming paradigms that change how you think about coding

#88

Post by jarrett »

JadeNB wrote: post #76
nuncanada wrote: post #67

Earlier quoted context omitted.

Yes, Depently Typed languages can. They are full blown theorem provers...

Gödel guarantees that full-blown theorem provers, even with human guidance, cannot prove all true statements about sufficiently rich systems. 'Sufficiently rich' here just means 'includes Peano arithmetic', and you can find tons of tutorials for doing just that (Church encoding) in even the simplest type systems. (This bit of pure-mathematics wonkery ignores the substance of jarrett's question, though; one doesn't ne…

> can never account for data that are provided only after compilation

It seems to me they could. Suppose my program depends on external input D. That input could be a file it loads, keyboard input, network input, or anything else. Could I declare that I expect D to have properties P? And then, could the language force me to implement a code path for cases where D does not satisfy P? An example of such a code path would be to print an error message and then terminate the program.

Re: Programming paradigms that change how you think about coding

#89

Post by AnimalMuppet »

danielweber wrote: post #55

I'm in the midst of something else and can't pull out my C++11 book now, but doesn't C++ have custom types that would let you declare something like "this must be a positive integer"? I might be confusing this with custom literals.

Well, there's unsigned integers. This means that it can't be less than 0. But if you have a 32 bit unsigned integer, and you decrement 0, you get 0xFFFFFFFF. That may or may not be what you want or expect.

You also could create a class that wrapped an integer, that would have a range, and would maintain that range as a class invariant. It could either clip or throw an exception when an attempt was made to go out of the range. But that's just regular class stuff, so I don't think it's what you had in mind...

Re: Programming paradigms that change how you think about coding

#90

Post by jarrett »

randyrand wrote: post #86
jarrett wrote: post #63

A thought on dependent types: Can a dependent type system catch all type errors at compile time? For example, suppose I write the following (in pseudo-code): // Variable x is an integer greater than or equal to 0 and less than 256. int x (>=0, I can imagine how a compiler could catch that kind of error. But that's trivial. What happens in programs like this: int x (>= 0, Now the compiler can't know for sure whether t…

| int x (>= 0, Will be a compile time error because getKeyBoard input returns integers that are between 0-256(?) not 0-10 like 'x' wants.

Exactly. That's why I proposed a Haskell-ish Maybe construct to represent the uncertainty of the input's validity. The code snippet:

  int x (>= 0,
...was meant as an example of what won't work.
Post reply on HN