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

141–150 of 206 posts

Re: Programming paradigms that change how you think about coding

#141

Post by tel »

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…

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.

Re: Programming paradigms that change how you think about coding

#142

Post by chriswarbo »

leoc wrote: post #120
arh68 wrote: post #92

Earlier quoted context omitted.

> 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).

Not quite. Many dependently-typed languages aren't Turing-complete, but that's no how they 'dodge this bullet'.

Think about the following Java code:

    public int getMyInt() {
      return getSomeOtherInt();
    }
How hard does Java have to work to figure out whether getMyInt is well-typed? Does it have to solve the halting problem? No. It just checks the information that you have given it. If you wrote that getSomeOtherInt has return type "int" then getMyInt will type-check. If you gave it some other type, it won't type-check. If you didn't give it a type, it will complain about a syntax error. At no point will Java try to write your program for you (which would hit against the halting problem). The same is true in dependently-typed languages, except the types happen to be much stronger. You still have to write them down, write down values of those types, write conversion functions when you need to combine different types, etc.

Incidentally, if a language is Turing-complete, it actually becomes really easy to get a program to type-check; we just write infinite loops everywhere, which leads to logical fallacies ;) That's why many dependently-typed languages aren't Turing-complete (although many are; eg. those which distinguish compile-time terms from run-time terms, like ATS).

Re: Programming paradigms that change how you think about coding

#143

Post by Dewie »

Dewie wrote: post #74
bnegreve wrote: post #57

Earlier quoted context omitted.

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 some…

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

EDIT: turns out that there kind of is:

http://nautilus.cs.miyazaki-u.ac.jp/cgi-bin/MagicHaskeller.c...

Re: Programming paradigms that change how you think about coding

#144

Post by dllthomas »

jessaustin wrote: post #134
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.

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 .

Hmm. Conceivably. I will have to revisit when I have more bandwidth.

Re: Programming paradigms that change how you think about coding

#145

Post by Kutta »

jessaustin wrote: post #134
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.

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 .

You're not misunderstanding. In short, we should rightfully expect our dependent type checker to be sound, if not complete. Weaker, non-dependent type systems can have complete checkers though, see for example

http://www.mpi-sws.org/~neelk/bidir.pdf

Re: Programming paradigms that change how you think about coding

#146

Post by hibikir »

archena wrote: post #52
SeanLuke wrote: post #37

> If you've used SQL, you've done a form of declarative programming This is so wrong I don't know where to begin.

Why do you think SQL doesn't qualify? it's certainly not the only example of declarative programming, and maybe not the most interesting, but it is one which most developers have come across.

In theory, SQL is a declarative programming language, in practice, past the simplest of examples, there are dozens, if not hundreds of ways to ask the same question, and each one of them performs differently. The moment one starts to do things like add anonymous views, the declarative facade tends to disappear.

Let's also remember that many companies stuck with big RDBMs systems have entire teams of people whose job includes turning declarative statements into extremely procedural ones.

So in practice, writing a SQL statement has little to do with making a query readable, but with abusing knowledge of internals to make it work fast. So declarative, not so much.

Re: Programming paradigms that change how you think about coding

#148

Post by arjunnarayan »

solomatov wrote: post #125
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.

>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 the most simple of invariants.

There's a reason dependent types haven't caught on in industry, and even the "fancy" types that are cited by proponents as being used in practice (like ML's Hindley-Milner type system) are MUCH simpler than full blown dependent type systems. Because the burden is shifted to the programmer, and that makes it super unusable.

I'm not a dependent types hater. (I have dependent type friends :) ). But the best way to get a usable type system is to restrict it's expressivity to make automation easier, and the annotation burden much smaller. Sure, we're giving up something there. But it's better than having a system that can prove any theorem in the Calculus of Constructions, but used by about thirty people.

Re: Programming paradigms that change how you think about coding

#149

Post by singold »

segmondy wrote: post #131
saosebastiao wrote: post #103

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…

How/where do you recommend to learn prolog? The concept looks really interesting and useful, at least for me.

Re: Programming paradigms that change how you think about coding

#150

Post by rybosome »

chriswarbo wrote: post #132
rybosome wrote: post #104

Earlier quoted context omitted.

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…

Makes sense; thanks for the clarification!
Post reply on HN