On Fri, 2007-10-12 at 13:52 -0400, 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
Manuel M T Chakravarty writes:
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
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
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
And Haskell embedded a logical programming language on accident.
On 10/15/07, Manuel M T Chakravarty [EMAIL PROTECTED] wrote:
Dan Piponi wrote,
On 10/12/07, Brandon S. Allbery KF8NH [EMAIL PROTECTED] wrote:
He wants to write entire programs in the type system,
something like the crazies
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* [EMAIL PROTECTED]
mailto:[EMAIL PROTECTED] wrote:
Dan Piponi wrote,
On 10/12/07, Brandon S. Allbery KF8NH
Dan Piponi wrote,
On 10/12/07, Brandon S. Allbery KF8NH [EMAIL PROTECTED] 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? :-)
Andrew Coppin 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
Current GHC can approximate this with a GADT:
==
{-# OPTIONS -fglasgow-exts #-}
module SafeHead where
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
On 10/12/07, Andrew Coppin [EMAIL PROTECTED] 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. You know,
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. You know, instead of the elaborate simulations crafted out
of systems
On 10/12/07, Steve Schafer [EMAIL PROTECTED] 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 -
On 10/12/07, Steve Schafer [EMAIL PROTECTED] 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
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
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
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
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
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. That the
Instant Insanity problem _was_ solved using Haskell's
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
On Oct 12, 2007, at 16:25 , Tim Chevalier wrote:
On 10/12/07, Steve Schafer [EMAIL PROTECTED] 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
On 10/12/07, Brandon S. Allbery KF8NH [EMAIL PROTECTED] 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
On Oct 12, 2007, at 19:26 , Tim Chevalier wrote:
On 10/12/07, Brandon S. Allbery KF8NH [EMAIL PROTECTED] 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
On 10/12/07, Brandon S. Allbery KF8NH [EMAIL PROTECTED] 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? :-)
On Oct 12, 2007, at 19:42 , Dan Piponi wrote:
On 10/12/07, Brandon S. Allbery KF8NH [EMAIL PROTECTED] 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
24 matches
Mail list logo
