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

111–120 of 206 posts

Re: Programming paradigms that change how you think about coding

#111

Post by Kutta »

arjunnarayan wrote: post #93
jarrett wrote: post #87

Earlier quoted context omitted.

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

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.

Note though that undecidability is not really an issue in practice. You can always just refuse to run any function compile time that has not yet passed termination check. In fact Idris does exactly this. This already puts Idris ahead of C++ in terms of compilation termination, and it's not even like people are frequently disgruntled about diverging C++ templates.

Re: Programming paradigms that change how you think about coding

#112

Post by cpa »

Dewie wrote: post #105
JadeNB wrote: post #76

Earlier quoted context omitted.

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…

I wonder; have mathematicians found something that they know with every fibre of their being is true, but that they can't prove? And do they then try to prove it in another formal system instead? Or do these unprovable-but-true facts mostly elude them, since they are operating in a formal system that 'hides' them?

Mathematicians say that formula F is true in system S iff one can find a proof of F in the context S. So truthness is always considered with respect to some system. Thus, there are no formula which is "true" but that one can't prove, by definition. (That's the kind of smartassery mathematicians like.)

But the Godel's incompleteness theorem states that for all system that includes (Peano's) arithmetic, one can find a formula in this system that has cannot be proved and whose contrary cannot be proved either. And to answer your question, Godel's proof explicitly shows such a formula.

Re: Programming paradigms that change how you think about coding

#113

Post by adambard »

prawks wrote: post #32
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…

The digital media department at my alma mater used Max/MSP to teach programming to art students with a lot of success. It's really fascinating to watch the programs as they run, and it makes for a great way to visualize abstraction and separation of concerns in a concrete way.

My degree included a "Computer Music" option, which were a few classes that were half music students and half computer science ones. We used Max/MSP quite a bit.

For anyone that wants to play around with a very similar language, PureData is an open-source application that is a relative of Max/MSP (they share a creator, and are quite similar). Not wanting to come in to do the homework or purchase the software myself, I used it quite a bit.

http://puredata.info/

Re: Programming paradigms that change how you think about coding

#114

Post by Orangeair »

seanmcdirmid wrote: post #34
bru wrote: post #3

Some notes: - parallel and concurrent are 2 different things - the 'symbolic languages' definition seems off. Wikipedia puts it right: > symbolic programming is computer programming in which the program can manipulate formulas and program components as data So it's not "using graphs & such to program"

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/

Re: Programming paradigms that change how you think about coding

#115

Post by dllthomas »

Kutta wrote: post #111
arjunnarayan wrote: post #93

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.

Note though that undecidability is not really an issue in practice. You can always just refuse to run any function compile time that has not yet passed termination check. In fact Idris does exactly this. This already puts Idris ahead of C++ in terms of compilation termination, and it's not even like people are frequently disgruntled about diverging C++ templates.

"You can always just refuse to run any function compile time that has not yet passed termination check."

I don't understand this sentence.

Re: Programming paradigms that change how you think about coding

#116

Post by josephschmoe »

Code Search is a better way to do Declarative Programming for non-optimized solutions. I've been obsessing over this topic for the last few months. Right now there's limited versions in a few places: Python's howdoi and Visual Studio's Code Search.

A true Code Search would work like this: 1. Type in your search term in your code in a comment line. i.e. "Bubble sort StampArray by name" 2. Google/Bing/StackOverflow searches for your string. Replaces your terms with generics. Searches for "Bubble sort [an array of objects] by [string variable]" 3. Takes code results and shows them to you. Replaces all instances of [string variable] with getName() and all instances of [Object[]] with StampArray. 4. You pick your favorite. 5. Your IDE adds the code to a "code search module" which you can edit. 6. Your edits get added to the search database.

The best part? You could even put your Declarative Programming engine -inside- of the Search just by populating initial search results. What about better code coming to exist in the future, you say? Well, you don't necessarily have to keep the same result forever. If it's been deprecated, you can re-do the search.

Re: Programming paradigms that change how you think about coding

#117

Post by lmkg »

Dewie wrote: post #105
JadeNB wrote: post #76

Earlier quoted context omitted.

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…

I wonder; have mathematicians found something that they know with every fibre of their being is true, but that they can't prove? And do they then try to prove it in another formal system instead? Or do these unprovable-but-true facts mostly elude them, since they are operating in a formal system that 'hides' them?

There are a couple of statements that have been proven to be unprovable in the standard axiom set (ZF). The provability of the unprovability of unprovable statements is not guaranteed, but happens to be true for many of the more useful axioms.

The most common is the Axiom of Choice, which if true is incredibly convenient. For example, the Axiom of Choice implies that all Vector Spaces have a basis, which makes linear algebra tractable. Mathematicians generally accept it as true because it's useful and intuitively true, but it does have some consequences that are intuitively false, like the Banach-Tarski paradox. We even have a saying: "The Axiom of Choice is obviously true, the Well-Ordering Principle is obviously false, and Zorn's Lemma no one even knows." The implicit punchline being, these three things are logically equivalent because each implies the other.

Other axioms that are independent of ZF include the Continuum Hypothesis and the Axiom of Foundation. The Continuum Hypothesis says that there is no type of infinity that is larger than the cardinality of the Rationals and also smaller than the cardinality of the Reals. It doesn't make a damn lick of sense for such a type of infinity to exist, but it's not technically possible to disprove it. The Axiom of Foundation, in very simple terms, disallows objects like "the set that contains itself." Such sets are not constructable in ZF, and are logically impossible, but they are not technically disallowed.

Using "stronger" axiom sets to investigate the properties and consequences of these unprovable statements is common. Additionally, many automated theorem-provers include several of the more convenient axioms that aren't included in "regular" mathematics.

More reading: http://en.wikipedia.org/wiki/List_of_statements_undecidable_...

(Note: ZFC is ZF plus the Axiom of Choice; Choice is so damn convenient that the mathematics establishment usually accepts it by default, although proving that you don't need Choice to prove something is often seen as a worthwhile accomplishment.)

Re: Programming paradigms that change how you think about coding

#118

Post by swah »

adwn wrote: post #49
swah wrote: post #29

Earlier quoted context omitted.

I really enjoyed writing VHDL. I don't remember having problems with unknown values: we used only '0' and '1' for anything that's supposed to be synthesized. (For testbenches, everything goes..) Value set is ('U','X','0','1','Z','W','L','H','-') TYPE std_logic IS ( 'U', -- Uninitialized 'X', -- Forcing unknown '0', -- Forcing 0 '1', -- Forsing 1 'Z', -- High impedance 'W', -- Weak unknown 'L', -- Weak 0 'H', -- Weak…

VHDL has the same problem: signal x, y: std_logic; ... x will result in y getting the value '1' in simulation, but you don't know what it'll be for synthesis. So if you're unlucky, it'll simulate correctly but fail in hardware. Which is exactly what simulation should protect you from. And even if you assign only '0' and '1', you might get an 'X' from third-party IP cores.

Yep, I agree about IP cores, never really used something like that.

Re: Programming paradigms that change how you think about coding

#119

Post by Kutta »

dllthomas wrote: post #115
Kutta wrote: post #111

Earlier quoted context omitted.

Note though that undecidability is not really an issue in practice. You can always just refuse to run any function compile time that has not yet passed termination check. In fact Idris does exactly this. This already puts Idris ahead of C++ in terms of compilation termination, and it's not even like people are frequently disgruntled about diverging C++ templates.

"You can always just refuse to run any function compile time that has not yet passed termination check." I don't understand this sentence.

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 occasionally run Idris functions (that's what makes it dependent). This is in fact the only source of potential non-termination in the checker. So, whenever Idris needs to run a function compile time, and it cannot prove termination via the checker, it just throws an error.

(Side note: it is never required to run a function in order to the typecheck the very same function. All major dependent type checkers has the property that they never have to run a function that is not already checked).

Re: Programming paradigms that change how you think about coding

#120

Post by leoc »

arh68 wrote: post #92
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? I'm probably not clever enough, but someone could probably prove that'd be equivalent to solving the halting problem. It seems impossible. > because the value of getKeyboardInput could be anything That makes my brain hurt. I think implicitly narrowing the type is stylistically better. Maybe just adding a dependent type declaration: x = (parseInt(get…

> I'm probably not clever enough, but someone could probably prove that'd be equivalent to solving the halting problem. It seems impossible.

IIRC dependently-typed languages dodge this bullet by not being completely Turing-complete (as 'twere).

Post reply on HN