Live data from Hacker News

Programming paradigms that change how you think about coding

brikis98.blogspot.com

131–140 of 206 posts

Re: Programming paradigms that change how you think about coding

#131

I'm a huge fan of the declarative programming paradigm, but outside of Regexp and SQL and a handful of other DSLs, it's dead. Its death should be a case study in Open Source strategy: It died because it became boring before it became useful. SQL and Regexp have stuck around because they did something useful immediately. I think that any future that the Declarative paradigm has within general purpose languages is the…

You are very mistaken. Prolog is still very much alive. You can find us on ##prolog in freenode. You can build a web application with prolog. When the 2048 madness was going on, I implemented in prolog in about 200 lines in 2 hours and I had about 3 weeks of prolog under my belt at that time. It's a very powerful concept. I didn't have to figure out the how to implement it, I just broke 2048 down into rules, declared it, and bam, I had a game.

Re: Programming paradigms that change how you think about coding

#132
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…

As others have noted, it's less about the compiler running code and making determinations as it is using extremely robust, information-rich types. For instance, the Vector type in Idris has two type parameters (not sure that's the correct term to use in this case): the first is the type of the element contained by the vector, and the second is the length of the vector. Operations that increase the size of the vector…

> For instance, the Vector type in Idris has two type parameters (not sure that's the correct term to use in this case): the first is the type of the element contained by the vector, and the second is the length of the vector.

In case anyone's wondering, only the first of these (the element type) is a type parameter, since it has a constant value in all sub-expressions (ie. the cons cells all contain elements of the same type).

The second is a 'type index', which is a more general term (type parameters are a special case of type indices), since its value changes in the sub-expressions (the cons cells have different lengths).

The difference is that we don't need to pattern-match parameters on every recursive call, since they're guaranteed to be constant (although we can if we like).

I didn't know this until I asked http://cs.stackexchange.com/questions/20100/what-are-the-dif...

Re: Programming paradigms that change how you think about coding

#133

Earlier quoted context omitted.

Mathematica is a good example of a symbolic language (can't get more symbolic than term rewriting), but he calls that....knowledge oriented or some other nonsense.

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/

Re: Programming paradigms that change how you think about coding

#134
post #119

Earlier quoted context omitted.

Both Idris and Agda check whether functions provably terminate. Halting problem notwithstanding it is possible to have conservative checks that never return false positives, so that an OK from the checker implies termination, but a FAIL doesn't imply non-termination. Idris is not total by default, so it is not required that all functions pass the termination check. However, when Idris does the type checking it has to…

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.

Maybe I'm misunderstanding, but Kutta's description seems to handle 1) and 2) just fine. An additional requirement of "guaranteeing 'yes' on every correctly typed program" would lead to contradiction, but the point is that you don't need that requirement in practice.

Re: Programming paradigms that change how you think about coding

#135
post #6
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?

As I mentioned in my other comment Verilog and VHDL are "concurrent by default" since that's how hardware works anyway. If you want to experiment with them you don't need an FPGA, you can just start with a simulator such as Icarus Verilog[1] and a waveform viewer like gtkwave[2] and get a feel of the language. There are a bunch of tutorials on the net. [1] http://iverilog.icarus.com/ [2] http://gtkwave.sourceforge.ne…

http://www.edaplayground.com/ is a great way to play with hardware description languages too. You don't need to install anything.

Re: Programming paradigms that change how you think about coding

#136
post #122

Earlier quoted context omitted.

The problem with theorem provers like Adga and Coq is they are brittle to refactoring and thus hard to make changes to an app. Something seeming small can ripple through the whole system. I hear Idris is more reasonable in this regard and has better general purpose programming properties.

>The problem with theorem provers like Adga and Coq is they are brittle to refactoring and thus hard to make changes to an app. Something seeming small can ripple through the whole system. I hear Idris is more reasonable in this regard and has better general purpose programming properties. You can say the same for any strongly typed language, but reality is it's the opposite. If your program has a good design, it's e…

source: http://www.johndcook.com/blog/2014/02/10/real-world-haskell/...

Re: Programming paradigms that change how you think about coding

#137

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.

>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 with a strict reading. "In general, dependent types ..." should be a statement about all instances of "dependent types" or (weakening to one common English usage) a statement about typical instances of "dependent types". In neither case, are they undecidable.

A loose reading (probably overly loose, but possibly what was intended rather than what was expressed) would permit something closer to "Dependent types, in full generality, are undecidable to type check." which I believe to be the case, where actual implementations are more constrained (though decreasingly so!).

Re: Programming paradigms that change how you think about coding

#138

Isn't "Dependent types" just re-inventing how Fortran handles non allocatable array and character variables i.e. those who's length is declared at compile time using a parameter?

Short answer: No.

Longer answer: Sort of. An array has an element type and length associated with it (and it ATS at least, the type-level length isn't kept at run-time) and that length is set when the array is created, and modified if elements are added or removed. However, functions can require parameter types or provide return values of "array T n | n > 0 && n There's a good deal more to dependent types, but they are much more flexible than simply attaching the length of the array to its type.

Re: Programming paradigms that change how you think about coding

#139

Where is Aspect Oriented Programming and all the other offspring of the Inversion of Control pattern (Dependency Injection, Dependency Inversion, ...)? Is this line of evolution in languages considered dead?

Yes, thank heavens, yes!

These are more tactical (i.e. low-level) techniques that big strategies that encapsulate entire languages.

Re: Programming paradigms that change how you think about coding

#140

Where is Aspect Oriented Programming and all the other offspring of the Inversion of Control pattern (Dependency Injection, Dependency Inversion, ...)? Is this line of evolution in languages considered dead?

Yes, thank heavens, yes!

What, you don't like computed non-local come-from's?
Post reply on HN