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

Re: Programming paradigms that change how you think about coding

#161

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

Someone wrote: post #160

dllthomas wrote: post #123

Earlier quoted context omitted.

So that was "You can always just refuse to run any function [at] compile time that has not yet passed termination check."? All of this is certainly the case, and useful, and interesting. It doesn't contradict the point that 1) guaranteeing termination and 2) guaranteeing you return "no" on every incorrectly typed program are incompatible, which was approximately the original question.

"1) guaranteeing termination and 2) guaranteeing you return "no" on every incorrectly typed program are incompatible" You do need more bandwidth. Trivial counterexample (for any reasonable inference of the semantics of the source code of this made-up language): define isCorrectlyTyped( program P) as return "no". Of course, a practical version would have to have the function return "yes" on more valid programs :-) By…

Fair point! I was wrong above - "Can a dependent type system catch all type errors at compile time?" Yes, so long as you're okay with rejecting some correctly typed programs! If you're not okay with that, then your type checker might not halt. Shame it's too late to add an addendum above...

Re: Programming paradigms that change how you think about coding

#162

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

tel wrote: post #141

vilhelm_s wrote: post #79

Earlier quoted context omitted.

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…

Yeah, less power means greater inference. You can model liquid types in a DT language I believe, but you'll never have the same convenience.

"Dependent types" is a quite broad term. The Liquid types people certainly call their work dependent types, even though it has a different flavour than e.g. Coq or Agda.

Re: Programming paradigms that change how you think about coding

#163

Post by mjcohen » Thu, Apr 10, 2014, 10:19 PM UTC

Serow225 wrote: post #19

Blahah wrote: post #4

The concurrent by default paradigm looks like it could be really useful for some cases. Does anyone know of any more well-used languages that support it?

Is Labview concurrent by default?

Yes. I enjoyed watching LV code execute graphically.

Re: Programming paradigms that change how you think about coding

#164

Post by tel » Thu, Apr 10, 2014, 10:33 PM UTC

vilhelm_s wrote: post #162

tel wrote: post #141

Earlier quoted context omitted.

Yeah, less power means greater inference. You can model liquid types in a DT language I believe, but you'll never have the same convenience.

"Dependent types" is a quite broad term. The Liquid types people certainly call their work dependent types, even though it has a different flavour than e.g. Coq or Agda.

Yes, that's true—I lapsed in terminology. Maybe calling it ITT would be better? There's a lot of ambiguity there, of course. And less marketing.

Re: Programming paradigms that change how you think about coding

#165

Post by solomatov » Thu, Apr 10, 2014, 10:33 PM UTC

arjunnarayan wrote: post #148

solomatov wrote: post #125

Earlier quoted context omitted.

>Basically, yes. If you want your type checker to be decidable, you're going to have to restrict the type language to be much smaller. In general, dependent types are undecidable to type check. In dependently typed programming languages like agda and Idris typechecking is decidable. You are wrong here.

You're right. I was being handwavey, and I apologize for that. Let me clarify my position: In theory yes, you're right, it is decidable. In practice Agda and Coq force you to prove pretty much everything about your program using expensive annotations, in order to satisfy the typechecker. It's like pulling teeth. The type checker must be taught that your program terminates, and it must be taught that you maintain even…

>Let me clarify my position: In theory yes, you're right, it is decidable. In practice Agda and Coq force you to prove pretty much everything about your program using expensive annotations, in order to satisfy the typechecker. It's like pulling teeth. The type checker must be taught that your program terminates, and it must be taught that you maintain even the most simple of invariants.

That's why we need gradual typing. Some critical parts should be written with full dependent types with termination checker, etc, but most of the code should be just type checked.

P.S. I have some dependent types experience, including applying Coq in commercial projects.

Re: Programming paradigms that change how you think about coding

#166

Post by jberryman » Thu, Apr 10, 2014, 10:51 PM UTC

Blahah wrote: post #4

The concurrent by default paradigm looks like it could be really useful for some cases. Does anyone know of any more well-used languages that support it?

Haskell's Par monad gives you a nice eDSL that lets you lay out your data dependencies and have things evaluated in parallel

http://hackage.haskell.org/package/monad-par-0.3.4.6/docs/Co...

Re: Programming paradigms that change how you think about coding

#167

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

milliams wrote: post #40

QML [1] is an interesting example of declarative programming. It allows constraints and relationships to be defined and the runtime will do the rest. Perhaps it's not as powerful as other languages but in its domain it does very well. [1] https://en.wikipedia.org/wiki/Qt_Modeling_Language

QML is simply brilliant for developing UIs.

Re: Programming paradigms that change how you think about coding

#168

Post by humanrebar » Thu, Apr 10, 2014, 11:04 PM UTC

lolo_ wrote: post #21

I think an underrated non-standard approach to programming is graphical programming. Though this approach doesn't seem to received significant uptake amongst professional programmers, there is an application called max [0] that is popular amongst musicians and artists and quite surprisingly powerful and effective. There's an interesting article [1] on how Jonny Greenwood of Radiohead uses it extensively, in there you…

I've used graphical programming in the past. It sounds amazing in abstract, but ends up being a mess when it is implemented. It basically requires a "sufficiently smart editor", which, even if implemented perfectly, would not leave a lot of room for a third-party ecosystem to be built around the language.

There are many solved problems in text-based programming that would need to be resolved in order for a graphical programming language to be as useful.

How would one post a "snippet" to StackOverflow? How would diffs work? Consequently, how would source code management work?

Re: Programming paradigms that change how you think about coding

#169

Post by seanmcdirmid » Thu, Apr 10, 2014, 11:42 PM UTC

taliesinb wrote: post #133

Orangeair wrote: post #114

Earlier quoted context omitted.

Mathematica[0] and The Wolfram Language[1] are two different things. The Wolfram Language is a sort of extension of their Wolfram Alpha service, which Wolfram itself describes as "Knowledge Based." Mathematica is still just Mathematica. [0] http://www.wolfram.com/mathematica/ [1] https://www.wolfram.com/language/

No. Mathematica is a commercial piece of desktop software that uses the Wolfram Language. Just like how RStudio uses R. There are other product platforms (coming soon) that employ the Wolfram Language, both in cloud and desktop incarnations: http://www.wolframcloud.com/

I'm not great at following markitecture, but didn't Mathematica exist and have a language before this language was rebraded as the Wolfram Language? There is nothing really wrong with this, but its understandable that people might be confused about it right now.

Re: Programming paradigms that change how you think about coding

#170

Post by seanmcdirmid » Thu, Apr 10, 2014, 11:48 PM UTC

segmondy wrote: post #157

saosebastiao wrote: post #151

Earlier quoted context omitted.

I never said it wasnt useful, I said that it was dead...much in the same sense as COBOL. I use datalog and constraint programming extensively, but I'm a black sheep.

It's not dead, until no one is using it. You can say APL is dead and I might believe you. So long as there's still people using prolog or other form of logic programming. It's not dead, all it needs is one killer application and everyone will jump on it. Erlang's popularity has surged since Whatsapp got acquired. Lots of people are learning about Erlang's root from Prolog and likewise getting somewhat curious about P…

APL is far from dead, there is a lot of living legacy code and old timers with APL skills still actively using it commercially.

Prolog on the other hand...I'm not aware of any commercial projects actively using it, but it is still alive as a hobbyist/learning language.