Programming paradigms that change how you think about coding • Hacker News Board

Re: Programming paradigms that change how you think about coding

#71

Post by zwieback » Thu, Apr 10, 2014, 3:50 PM UTC

simias wrote: post #53

adwn wrote: post #25

Earlier quoted context omitted.

... and then suddenly you realize what a horrible, horrible language it is. I'm not exaggerating, it isn't even well-suited for the domain it is mainly used for (i.e., designing digital hardware circuits). For example: 1) Synthesis/simulation mismatch: Your design might work in simulation but not in hardware, and vice versa . Often, this is due to X-value (representing unknown/invalid values) problems. 2) Signed data…

Oh I agree, while writing verilog I was amazed people used it to develop something as critical as ASICs. The language is way too forgiving. And it's not like you can release a patch once the thing is on the silicium unless you're working with FPGAs. It was still very interesting to see how hardware was designed and definitely an enlightening experience as far as I'm concerned. I found verilog very similar to C in a w…

This seems true for other areas of EE. I'm continually surprised that our FPGA and board designers use some adhoc horrible homegrown revision control scheme. When I ask them about tools of the trade they usually complain that the solutions are proprietary and not working any better than making numbered backups.

The same is true, maybe even worse, for our MEs.

Re: Programming paradigms that change how you think about coding

#72

Post by JoshTriplett » Thu, Apr 10, 2014, 3:52 PM UTC

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…

The compiler doesn't necessarily have to have that level of inference; it can simply require the code to prove the constraints. For instance, parseInt will return an unconstrained int, so you'll get a type error trying to assign that to a range-constrained int. For your first and last examples, the multiplication operator on range-constrained ints can easily propagate the range constraints. In your last example, `z = w * x` would work, but assigning through the unconstrained int y may simply cause the last assignment z=y to produce a type error, forcing the code to re-establish the constraint explicitly.

Re: Programming paradigms that change how you think about coding

#73

Post by zwieback » Thu, Apr 10, 2014, 3:53 PM UTC

glifchits wrote: post #59

jameshart wrote: post #10

This is a substantial piece of writing with information many here would find interesting; putting it behind a buzzfeed list style headline does it a disservice. One step short of calling it "Six weird programming paradigms that will blow your mind".

Just because Buzzfeed uses list style headlines and has vacuous content does not mean that list style headlines are an indicator of vacuous content. If you read this and you liked it, does the title really matter?

Exactly. Plus, while the content might be vacuous it's often quite entertaining and the editorial style is genius, in my opinion. I think writers can probably learn 41 things from Buzzfeed.

Re: Programming paradigms that change how you think about coding

#74

Post by Dewie » Thu, Apr 10, 2014, 3:54 PM UTC

bnegreve wrote: post #57

cjfont wrote: post #54

Earlier quoted context omitted.

Seems pretty obvious to me, since the above description could also apply to your typical declarative languages such as SQL, where you also rely on the database to do optimizations based on a description of the result you're looking for, rather than procedures for calculating it.

Just to clarify, it wasn't obvious to me before I read the part of the article that I have quoted. But I still think that functional programming goes beyond simply specifying "what you want". Take the problem of sorting an array for example. A declarative specification of the sorting problem would be: Given an array T, compute a permutation of T such that for all i, it's true that T[i] Clearly here, you don't describ…

IMO the way that functional programming is declarative is that you can spell functions out like definitions. Like "fac(x) is

¤ 1 if x == 1

¤ x * fac(x-1) otherwise"

This is at least more declarative than describing the function with a loop. With an imperative program you kind of have to describe as a series of steps, because the order matters so much.

Personally I prefer this kind of declarative programming over something like Prolog since I get a simple way of describing what/how the program is, while still feeling declarative. With Prolog I still have to learn how it works, and the way that it works is more removed from imperative and functional programming (while functional programming can be done (maybe with, but in principle) in most imperative languages as long as you restrict your use of certain features). Plus Prolog has un-declarative things like the cut operator. I don't really have much experience with declarative programming outside of these two.

Something more declarative might indeed just be to give invariants and let the program find an implementation for it.

Re: Programming paradigms that change how you think about coding

#75

Post by dllthomas » Thu, Apr 10, 2014, 4:00 PM UTC

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.

Re: Programming paradigms that change how you think about coding

#76

Post by JadeNB » Thu, Apr 10, 2014, 4:04 PM UTC

nuncanada wrote: post #67

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, 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 need the full Gödelian power to observe that a priori theorems that must be verified at compile time can never account for data that are provided only after compilation.)

Re: Programming paradigms that change how you think about coding

#77

Post by ardz » Thu, Apr 10, 2014, 4:07 PM UTC

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…

In DT languages you can even do something like: x of type: > 0, skyIsBlueNow().

Re: Programming paradigms that change how you think about coding

#78

Post by JadeNB » Thu, Apr 10, 2014, 4:07 PM UTC

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…

Without really addressing your question, notice that the power of dependently typed languages is not in the intelligence of the compiler, but in the expressivity of the type system. That is, the question becomes not "can the compiler catch this error on its own?", but rather "can the compiler verify my proof that I have not made this error?" A language with a very powerful type system can still have a very dumb compiler (although it will generate extremely slow code).

EDIT: It occurs to me that this is well summarised by the apparently facetious remark "Ask not what your compiler can do for you; ask what you can do for your compiler."

Re: Programming paradigms that change how you think about coding

#79

Post by vilhelm_s » Thu, Apr 10, 2014, 4:12 PM UTC

tel wrote: post #68

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…

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 Their latest research language is "Liquid Haskell", I think it could deal with jarrett's example out of the box (with the caveat that yes, you still need to write the test explicitly). They used to have an online demo where you could just type programs into a web form, but that doesn't seem to work right now...

Re: Programming paradigms that change how you think about coding

#80

Post by protomyth » Thu, Apr 10, 2014, 4:15 PM UTC

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.