On 10/12/07, Steve Schafer wrote:

On Fri, 12 Oct 2007 18:24:38 +0100, you wrote:

...

I was actually thinking more along the lines of a programming language where you can just write

head :: (n > 1) => List n x -> x

tail :: List n x -> List (n-1) x

(++) :: List n x -> List m x -> List (n+m) x

and so forth.

How, then, is that any different from a general-purpose programming language?

It's different because the property that (for example) head requires a nonempty list is checked at compile time instead of run time.

You're just drawing the "line in the sand" in a different place. You end up with a programming system where compilation is a "side effect" of executing the "real" program.

I'm not sure exactly what you mean by that, but a lot of people are spending time thinking about ways for programmers to express more of their knowledge about programs in a way that's accessible to and checkable by compilers and other automated tools, and while you might see it as "just drawing the line in the sand in a different place", you could say the same thing about programming in a language with a Haskell-like type system instead of a Lisp-like type system. Cheers, Tim -- Tim Chevalier * catamorphism.org * Often in error, never in doubt "Yeah. Okay. Yeah. Basically, swingers meet ISO 9000." -- DF, on cuddle parties

On 10/12/07, Steve Schafer wrote:

On Fri, 12 Oct 2007 13:03:16 -0700, you wrote:

...

It's different because the property that (for example) head requires a nonempty list is checked at compile time instead of run time.

No, I understand that. Andrew was talking about using type programming to do the things that a sane person would use "ordinary" programming to do.

I'm not sure what sanity has to do with it. Presumably we all agree that it's a good idea for the compiler to know, at compile-time, that head is only applied to lists. Why not also have the compiler check that head is only applied to non-empty lists? If you think it's sane to want one property checked at compile-time and insane to want the other property checked at compile-time, can you describe your test that can be applied to program properties to determine whether or not it's sane to want them statically checked?

And he wanted to know if there were any efforts to create a type system syntax that better supported that. But it seems to me that when you do that, the language of the type system begins to look like a general-purpose programming language. And that just shoves everything up to the next "meta" level. Pretty soon, you're going to need a meta-type system to meta-type-check your type language, and so on.

This criticism has been made before.

I'm all for enhancing the expressibility of concepts _related to typing_ within the type system, but I don't think that was the original point of this discussion. After all, Andrew's original message mentioned "stuff the type system was never designed to do."

What do you mean by "related to typing"? Haskell's type system allows us to say that head is a function that maps a list of things of type a onto a thing of type a. A more expressive type system might allow us to say that head's domain consists of *non-empty* lists. In this type system, emptiness or non-emptiness is "a concept related to typing", because it's a concept that that type system can express. You seem to be criticizing richer type systems on the sole basis that they are richer than existing ones. Cheers, Tim -- Tim Chevalier * catamorphism.org * Often in error, never in doubt "I always wanted to be commander-in-chief of my own one-woman army" -- Ani DiFranco

On Fri, 12 Oct 2007, Steve Schafer wrote:

On Fri, 12 Oct 2007 13:25:28 -0700, you wrote:

...

I'm not sure what sanity has to do with it. Presumably we all agree that it's a good idea for the compiler to know, at compile-time, that head is only applied to lists. Why not also have the compiler check that head is only applied to non-empty lists?

Again, that sort of practical application of type systems is not (as far as I know) what this discussion is about. This discussion was spawned by talk of using the type system to do truly bizarre things, such as solve the Instant Insanity puzzle. A while back, Dan Piponi posed the question of using the type system to solve one of the liar/truthteller logic problems. And so on.

Which is nevertheless the kind of power you need in order to also be able to prove precise properties. How are you going to prove that an entire class of problems is solveable (and the safety or termination of a piece of code may depend on this) if you can't prove that an individual one is? -- flippa@flippac.org A problem that's all in your head is still a problem. Brain damage is but one form of mind damage.

On Fri, 12 Oct 2007, Steve Schafer wrote:

On Fri, 12 Oct 2007 21:51:46 +0100 (GMT Daylight Time), you wrote:

...

Which is nevertheless the kind of power you need in order to also be able to prove precise properties.

We're not talking about POWER, we're talking about SYNTAX.

Which has no small amount to do with the power to express problems in a natural way, no? My point being that we already want this for things that are more obviously appropriate uses of a type system.

To which my rejoinder is, "To what end?" To extend the _syntax_ of the type system in a way that allows such "natural" expression turns it into yet another programming language. So what have we gained?

It's already yet another programming language, whether you like it or not - the question is how usable it is. Either you accept the gains made on the way or not, but what we have gained is the ability to reason about our programs in the language they are written in. We already have types-of-types in Haskell, they're called kinds. There's even a language that'll let you stack this as far as you like - why not? Zero, one or infinity, what else is new? -- flippa@flippac.org Society does not owe people jobs. Society owes it to itself to find people jobs.

On 10/12/07, Brandon S. Allbery KF8NH wrote:

You two are talking past each other. You're talking about dependent typing, etc. Steve's complaint is not about dependent typing; he's saying Andrew is looking for something different from that, namely the type system being a metalanguage.

Well, the type system *is* a metalanguage, so presumably Andrew's looking for something more specific than that...

I have the same impression, that Andrew isn't interested in dependent typing.

I'm not sure what he was really asking in his OP either, but when he said that he was looking for a language where you can write type signatures that encode list length, that certainly points to dependent types as one instance of that, even if there are other possibilities. Cheers, Tim -- Tim Chevalier * catamorphism.org * Often in error, never in doubt "The way NT mounts filesystems is something I'd expect to find in a barnyard or on a stock-breeding farm."--Mike Andrews

On 10/12/07, Brandon S. Allbery KF8NH wrote:

He wants to write entire programs in the type system, something like the crazies who write programs in C++ templates such that template expansion does all the work at compile time

Crazies? :-) http://homepage.mac.com/sigfpe/Computing/peano.html Having switched from C++ to Haskell (at least in my spare time) I thought I'd escaped that kind of type hackery but it seems to be following me... -- Dan

Dan Piponi wrote,

On 10/12/07, Brandon S. Allbery KF8NH wrote:

...

He wants to write entire programs in the type system, something like the crazies who write programs in C++ templates such that template expansion does all the work at compile time

Crazies? :-) http://homepage.mac.com/sigfpe/Computing/peano.html

Having switched from C++ to Haskell (at least in my spare time) I thought I'd escaped that kind of type hackery but it seems to be following me...

The way I see, we are trying to come up with a clean way of providing type-level computations (ie, we use and extend the standard theory of HM type systems). C++ embedded a functional language in the type systems mostly by accident, whereas we do it on purpose. Manuel

Lennart Augustsson wrote,

And Haskell embedded a logical programming language on accident.

Well, we are just trying to fix that :)

On 10/15/07, *Manuel M T Chakravarty* mailto:chak@cse.unsw.edu.au> wrote:

Dan Piponi wrote, > On 10/12/07, Brandon S. Allbery KF8NH < allbery@ece.cmu.edu mailto:allbery@ece.cmu.edu> wrote: > >> He wants to write entire programs in the type system, >> something like the crazies who write programs in C++ templates such >> that template expansion does all the work at compile time > > Crazies? :-) > http://homepage.mac.com/sigfpe/Computing/peano.html > > Having switched from C++ to Haskell (at least in my spare time) I > thought I'd escaped that kind of type hackery but it seems to be > following me...

The way I see, we are trying to come up with a clean way of providing type-level computations (ie, we use and extend the standard theory of HM type systems). C++ embedded a functional language in the type systems mostly by accident, whereas we do it on purpose.

Manuel

Ross Paterson wrote,

On Tue, Oct 16, 2007 at 10:56:27AM +1000, Manuel M T Chakravarty wrote:

...

Lennart Augustsson wrote,

...

And Haskell embedded a logical programming language on accident. Well, we are just trying to fix that :)

Since types are inferred using unification, and classes are still present, adding functions yields a functional logic programming language at the type level.

I used to agree with that, but I changed my opinion. Or more precisely, I'd say that it is a very weak functional logic language. "Weak" in the sense that it's logic component is essential nil. Let me justify this statement. We have type variables that are like "logical variables" in logic programming languages. However, we never use function definitions to guess values for type variables. Instead, function evaluation simplify suspends when it depends on an uninstantiated variable and resumes when this variable becomes instantiated. (The functional logic people call this evaluation strategy "residuation".) For example, if we have type family T a type instance T Int = Char then, given (T a ~ Char), we do *not* execute T backwards and infer (a = Int). Instead, we leave (T a ~ Char) as it is and evaluate 'T' only when 'a' becomes fixed. There have been proposals for truely functional logic languages using residuation, but they include support for backtracking and producing multiple solutions to a single query. We support neither on the type level. So, the only interaction between type functions and unification left is that function evaluation suspends on uninstantiated type variables and resumes when they become instantiated. This is not functional logic programming, it is *concurrent* functional programming with single-assignment variables. In fact, languages such as Id and pH, which are routinely characterised as concurrent functional, use exactly this model. I don't think the presence of type classes *without* functional dependencies changes this. Manuel PS: You get a *real* functional logic language by truly performing unification modulo an equational theory. This leads to the concept of E-unification and, in our constructor-based context, to "narrowing" as an evaluation strategy.

Steve said:

How, then, is that any different from a general-purpose programming language? You're just drawing the "line in the sand" in a different place.

In a way it is like drawing a line in sand. But that's a useful thing to do for a bunch of reasons. (1) When developing code, you'd like to test as much of the code as possible for reliability. But you don't necessarily know what data your code is going to run on in the future. It'd be cool if you could somehow run as much of your code as possible even without yet having the data. By having a declaration like

(++) :: List n x -> List m x -> List (n+m) x

it's almost as if the compiler gets to run a 'reduced' version of your application. You don't actually know what the elements of the list are (or even their types), and yet you can still test to see if your code handles the lists of the lengths correctly. (2) Sometimes you want to solve a problem incrementally. It's often helpful to reason first to the type we want, and then the implementation, rather than just to the implementation - it gives a way to factor the problem into two stages. By allowing some computation to take place at compile time you can be flexible about where the boundaries between your stages lie allowing you much more freedom in how you incrementally arrive at your solution. (3) In theory you can get very efficient code out of a type system where the compiler knows, for example, how long the lists are in advance. I guess you could say it's a form of partial evaluation. -- Dan