Is "take" behaving correctly?

newer
haskell on llvm?

older
Memory leak or wrong use of Array ?

PR Stanley

11 Sep 2007 11 Sep '07

11:05 p.m.

Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. Any ideas? Thanks, Paul

Show replies by date

Tim Chevalier

11 Sep 11 Sep

11:08 p.m.

On 9/11/07, PR Stanley wrote:

...

Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. Any ideas?

No, that's the behavior for take specified in the Haskell 98 report: http://haskell.org/onlinereport/standard-prelude.html "-- take n, applied to a list xs, returns the prefix of xs of length n, -- or xs itself if n > length xs." Cheers, Tim -- Tim Chevalier * catamorphism.org * Often in error, never in doubt "Modesty...is both alien and irrelevant to people who are happy in themselves, in their beings, in their skins, their natures, their capacities."--Anne Sayre

PR Stanley

11:39 p.m.

I suppose I'm thinking of head or tail - e.g. head [] or tail []. I'm trying to write my own version of the find function. I have a few ideas but not quite sure which would be more suitable in the context of FP. Any advice would be gratefully received - e.g. do I use recursion, list comprehension or what? Thanks, Paul At 00:08 12/09/2007, you wrote:

...

On 9/11/07, PR Stanley wrote:

...
Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. Any ideas?

No, that's the behavior for take specified in the Haskell 98 report: http://haskell.org/onlinereport/standard-prelude.html "-- take n, applied to a list xs, returns the prefix of xs of length n, -- or xs itself if n > length xs."

Cheers, Tim

-- Tim Chevalier * catamorphism.org * Often in error, never in doubt "Modesty...is both alien and irrelevant to people who are happy in themselves, in their beings, in their skins, their natures, their capacities."--Anne Sayre

Don Stewart

11:47 p.m.

prstanley:

...

I suppose I'm thinking of head or tail - e.g. head [] or tail []. I'm trying to write my own version of the find function. I have a few ideas but not quite sure which would be more suitable in the context of FP. Any advice would be gratefully received - e.g. do I use recursion, list comprehension or what?

Well, you want to filter all elements from a list that match a predicate, and then return Just the first match, or Nothing? find :: (a -> Bool) -> [a] -> Maybe a Checking the current behaviour: > find isSpace "haskell is fun" Just ' ' My first go would be something like this: ok, so let's start with 'filter': > filter Char.isSpace "haskell is fun" " " Good, then the natural translation to the Maybe type: > listToMaybe . filter isSpace $ "haskell is fun" Just ' ' And we're almost done. Just firing up QuickCheck: > quickCheck $ \p (xs :: [Int]) -> find p xs == listToMaybe (filter p xs) OK, passed 100 tests. Seems ok. I hope that gives some insight into the process of deriving Haskell implementations by building up a pipeline of pieces. -- Don

Brent Yorgey

11:38 p.m.

On 9/11/07, PR Stanley wrote:

...

Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. Any ideas? Thanks, Paul

If for some reason you want a version that does return an error in that situation, you could do something like the following: take' n _ | (n <= 0) = [] take' n [] | (n > 0) = error "take': list too short" | otherwise = [] take' n (x:xs) = x : take' (n-1) xs I'm not sure why you'd want that, though. The standard implementation gracefully handles all inputs, and usually turns out to be what you want. Really, if I were you, instead of making a version take' as above, I would just use the standard take but check for the length of the list in the places where it matters. -Brent

Don Stewart

11:40 p.m.

byorgey:

...

On 9/11/07, PR Stanley <[1]prstanley@ntlworld.com> wrote:

Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. Any ideas? Thanks, Paul

If for some reason you want a version that does return an error in that situation, you could do something like the following:

take' n _ | (n <= 0) = [] take' n [] | (n > 0) = error "take': list too short" | otherwise = [] take' n (x:xs) = x : take' (n-1) xs

And we'd call it unsafeTake, just like unsafeFromJust and unsafeTail :-) -- Don

Brent Yorgey

11:45 p.m.

On 9/11/07, Don Stewart wrote:

...

...
On 9/11/07, PR Stanley <[1]prstanley@ntlworld.com> wrote:

Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. Any ideas? Thanks, Paul

If for some reason you want a version that does return an error in

byorgey: that

...
situation, you could do something like the following:

take' n _ | (n <= 0) = [] take' n [] | (n > 0) = error "take': list too short" | otherwise = [] take' n (x:xs) = x : take' (n-1) xs

And we'd call it unsafeTake, just like unsafeFromJust and unsafeTail :-)

-- Don

Hmm, that's funny, I don't recall ever hearing of those functions... =) ooo, Don has a shiny new e-mail address! -Brent

Don Stewart

11:48 p.m.

byorgey:

...

On 9/11/07, Don Stewart <[1]dons@galois.com> wrote:

byorgey: > On 9/11/07, PR Stanley <[1]prstanley@[2]ntlworld.com> wrote: > > Hi > take 1000 [1..3] still yields [1,2,3] > I thought it was supposed to return an error. > Any ideas? > Thanks, Paul > > If for some reason you want a version that does return an error in that > situation, you could do something like the following: > > take' n _ | (n <= 0) = [] > take' n [] | (n > 0) = error "take': list too short" > | otherwise = [] > take' n (x:xs) = x : take' (n-1) xs

And we'd call it unsafeTake, just like unsafeFromJust and unsafeTail :-)

-- Don

Hmm, that's funny, I don't recall ever hearing of those functions... =)

ooo, Don has a shiny new e-mail address!

And a shiny new job in a shiny new city :-) -- Don

Derek Elkins

12 Sep 12 Sep

2:04 a.m.

On Tue, 2007-09-11 at 16:48 -0700, Don Stewart wrote:

...

byorgey:

...
On 9/11/07, Don Stewart <[1]dons@galois.com> wrote:

byorgey: > On 9/11/07, PR Stanley <[1]prstanley@[2]ntlworld.com> wrote: > > Hi > take 1000 [1..3] still yields [1,2,3] > I thought it was supposed to return an error. > Any ideas? > Thanks, Paul > > If for some reason you want a version that does return an error in that > situation, you could do something like the following: > > take' n _ | (n <= 0) = [] > take' n [] | (n > 0) = error "take': list too short" > | otherwise = [] > take' n (x:xs) = x : take' (n-1) xs

And we'd call it unsafeTake, just like unsafeFromJust and unsafeTail :-)

-- Don

Hmm, that's funny, I don't recall ever hearing of those functions... =)

ooo, Don has a shiny new e-mail address!

And a shiny new job in a shiny new city :-)

In a new country.

ok

10 p.m.

New subject: Monad.Reader 8: Haskell, the new C++

In Monad.Reader 8, Conrad Parker shows how to solve the Instant Insanity puzzle in the "Haskell" type system. Along the way he demonstrates very clearly something that was implicit in Mark Jones' "Type Classes with Functional Dependencies" paper if you read it very very carefully (which I hadn't, but on re-reading it is there). That is, Haskell types plus multiparameter type classes plus functional dependencies is a logic programming language. In fact it is a sufficiently powerful language to emulate any Turing machine calculation as a type checking problem. So we have C++ : imperative language whose type system is a Turing-complete functional language (with rather twisted syntax) Haskell: functional language whose type system is a Turing- complete logic programming language (with rather twisted syntax) Since not all Turing machines halt, and since the halting problem is undecidable, this means not only that some Haskell programs will make the type checker loop forever, but that there is no possible meta- checker that could warn us when that would happen. I've been told that functional dependencies are old hat and there is now something better. I suspect that "better" here means "worse".

Don Stewart

10:06 p.m.

New subject: Monad.Reader 8: Haskell, the new C++

ok:

...

In Monad.Reader 8, Conrad Parker shows how to solve the Instant Insanity puzzle in the "Haskell" type system. Along the way he demonstrates very clearly something that was implicit in Mark Jones' "Type Classes with Functional Dependencies" paper if you read it very very carefully (which I hadn't, but on re-reading it is there). That is, Haskell types plus multiparameter type classes plus functional dependencies is a logic programming language. In fact it is a sufficiently powerful language to emulate any Turing machine calculation as a type checking problem.

So we have

C++ : imperative language whose type system is a Turing-complete functional language (with rather twisted syntax)

Haskell: functional language whose type system is a Turing- complete logic programming language (with rather twisted syntax)

Since not all Turing machines halt, and since the halting problem is undecidable, this means not only that some Haskell programs will make the type checker loop forever, but that there is no possible meta- checker that could warn us when that would happen.

I've been told that functional dependencies are old hat and there is now something better. I suspect that "better" here means "worse".

Better here means "better" -- a functional language on the type system, to type a functional language on the value level. -- Don

Aaron Denney

11:36 p.m.

New subject: Monad.Reader 8: Haskell, the new C++

On 2007-09-12, Don Stewart wrote:

...

ok:

...
I've been told that functional dependencies are old hat and there is now something better. I suspect that "better" here means "worse".

Better here means "better" -- a functional language on the type system, to type a functional language on the value level.

Meh. I prefer functional languages for general problems, but as type-checking is a rather specific problem, I don't see why logic programming isn't more appropriate. -- Aaron Denney -><-

Derek Elkins

11:56 p.m.

New subject: Monad.Reader 8: Haskell, the new C++

On Wed, 2007-09-12 at 23:36 +0000, Aaron Denney wrote:

...

On 2007-09-12, Don Stewart wrote:

...
ok:

...
I've been told that functional dependencies are old hat and there is now something better. I suspect that "better" here means "worse".

Better here means "better" -- a functional language on the type system, to type a functional language on the value level.

Meh. I prefer functional languages for general problems, but as type-checking is a rather specific problem, I don't see why logic programming isn't more appropriate.

Type systems are the new general purpose programming languages.

Pepe Iborra

13 Sep 13 Sep

9:58 a.m.

New subject: Monad.Reader 8: Haskell, the new C++

On 13/09/2007, at 0:06, Don Stewart wrote:

...

ok:

...
In Monad.Reader 8, Conrad Parker shows how to solve the Instant Insanity puzzle in the "Haskell" type system. Along the way he demonstrates very clearly something that was implicit in Mark Jones' "Type Classes with Functional Dependencies" paper if you read it very very carefully (which I hadn't, but on re-reading it is there). That is, Haskell types plus multiparameter type classes plus functional dependencies is a logic programming language. In fact it is a sufficiently powerful language to emulate any Turing machine calculation as a type checking problem.

So we have

C++ : imperative language whose type system is a Turing-complete functional language (with rather twisted syntax)

Haskell: functional language whose type system is a Turing- complete logic programming language (with rather twisted syntax)

Since not all Turing machines halt, and since the halting problem is undecidable, this means not only that some Haskell programs will make the type checker loop forever, but that there is no possible meta- checker that could warn us when that would happen.

I've been told that functional dependencies are old hat and there is now something better. I suspect that "better" here means "worse".

Better here means "better" -- a functional language on the type system, to type a functional language on the value level.

-- Don

For a taste, see Instant Insanity transliterated in this functional language: http://hpaste.org/2689 NB: it took me 5 minutes, and that was my first piece of coding ever with Type families

Pepe Iborra

2:38 p.m.

New subject: Monad.Reader 8: Haskell, the new C++

...

For a taste, see Instant Insanity transliterated in this functional language:

http://hpaste.org/2689

I thought I'd better paste here the code for Instant Insanity with Type Families. Otherwise it will vanish in a short time. I took the opportunity to clean it up a bit. Although AT are not a supported feature, the code works in a 6.8.1 snapshot. But note that you cannot actually see the solution, as there is no way to ask GHCi to display the normalized types. My favorite bit is: *> type instance Map f Nil = Nil *> type instance Map f (x:::xs) = Apply f x ::: Map f xs \begin{code} import Prelude hiding (all, flip, map, filter) u = undefined data R -- Red data G -- Green data B -- Blue data W -- White data Cube u f r b l d type CubeRed = Cube R R R R R R type CubeBlue = Cube B B B B B B type Cube1 = Cube B G W G B R type Cube2 = Cube W G B W R R type Cube3 = Cube G W R B R R type Cube4 = Cube B R G G W W data True data False type family And b1 b2 type instance And True True = True type instance And True False= False type instance And False True = False type instance And False False= False data Nil data Cons x xs data x ::: xs infixr 5 ::: type family ListConcat l1 l2 type instance ListConcat Nil l = l type instance ListConcat (x:::xs) ys = x:::(ListConcat xs ys) type family Apply f a data Rotation data Twist data Flip type instance Apply Rotation (Cube u f r b l d) = Cube u r b l f d type instance Apply Twist (Cube u f r b l d) = Cube f r u l d b type instance Apply Flip (Cube u f r b l d) = Cube d l b r f u type family Map f xs type instance Map f Nil = Nil type instance Map f (x:::xs) = Apply f x ::: Map f xs type family Filter f xs type instance Filter f Nil = Nil type instance Filter f (x:::xs) = AppendIf (Apply f x) x (Filter f xs) type family AppendIf b x ys type instance AppendIf True x ys = x ::: ys type instance AppendIf False x ys = ys type family MapAppend f xs type instance MapAppend f Nil = Nil type instance MapAppend f (x:::xs) = ListConcat (x:::xs) (Map f (x:::xs)) type family MapAppend2 f xs type instance MapAppend2 f Nil = Nil type instance MapAppend2 f (x:::xs) = ListConcat (x:::xs) (MapAppend f (Map f (x:::xs))) type family MapAppend3 f xs type instance MapAppend3 f Nil = Nil type instance MapAppend3 f (x:::xs) = ListConcat xs (MapAppend2 f (Map f (x:::xs))) data Orientations type instance Apply Orientations c = MapAppend3 Rotation ( MapAppend2 Twist ( MapAppend Flip (c:::Nil))) type family NE x y type instance NE R R = False type instance NE R G = True type instance NE R B = True type instance NE R W = True type instance NE G R = True type instance NE G G = False type instance NE G B = True type instance NE G W = True type instance NE B R = True type instance NE B G = True type instance NE B B = False type instance NE B W = True type instance NE W R = True type instance NE W G = True type instance NE W B = True type instance NE W W = False type family All l type instance All Nil = True type instance All (False ::: xs) = False type instance All (True ::: xs) = All xs type family Compatible c1 c2 type instance Compatible (Cube u1 f1 r1 b1 l1 d1) (Cube u2 f2 r2 b2 l2 d2) = All (NE f1 f2 ::: NE r1 r2 ::: NE b1 b2 ::: NE l1 l2) type family Allowed c cs type instance Allowed c Nil = True type instance Allowed c (y ::: ys) = And (Compatible c y) (Allowed c ys) type family Solutions cs type instance Solutions Nil = (Nil ::: Nil) type instance Solutions (c ::: cs) = AllowedCombinations (Apply Orientations c) (Solutions cs) type family AllowedCombinations os sols type instance AllowedCombinations os Nil = Nil type instance AllowedCombinations os (s ::: sols) = ListConcat (AllowedCombinations os sols) (MatchingOrientations os s) type family MatchingOrientations os sol type instance MatchingOrientations Nil sol = Nil type instance MatchingOrientations (o ::: os) sol = AppendIf (Allowed o sol) (o:::sol) (MatchingOrientations os sol) type Cubes = (Cube1 ::: Cube2 ::: Cube3 ::: Cube4 ::: Nil) solution = u :: Solutions Cubes \end{code}

Manuel M T Chakravarty

14 Sep 14 Sep

1:05 a.m.

New subject: Monad.Reader 8: Haskell, the new C++

Pepe Iborra wrote,

...

...
For a taste, see Instant Insanity transliterated in this functional language:

http://hpaste.org/2689

I thought I'd better paste here the code for Instant Insanity with Type Families. Otherwise it will vanish in a short time. I took the opportunity to clean it up a bit.

Thanks!

...

Although AT are not a supported feature, the code works in a 6.8.1 snapshot. But note that you cannot actually see the solution, as there is no way to ask GHCi to display the normalized types.

Just to complete transferring the discussion from the ephemeral hpaste to the mailing list. My response to the lack of being able to display normalised types was that GHC actually goes to considerable trouble to preserve the original (non-normalised types) for error messages and other output, as this usually makes these messages easier to understand (eg, you usually rather like String than [Char] in an error message). However, to debug your type-level programs (or to abuse the type checker as an evaluator) this is clearly inconvenient. So, the plan is to add a ghci command that given a type will print its normal form. On hpaste, Pepe also suggested a flag to instruct the compiler to generally print normalised instead of unnormalised types. However, I think a form of eval for types on the command line is the most direct way of experimenting with type families and debugging type-level programs. Manuel PS: And, no, you won't be able to set breakpoints in type-level programs...

Stefan O'Rear

1:39 a.m.

New subject: Monad.Reader 8: Haskell, the new C++

On Fri, Sep 14, 2007 at 11:05:34AM +1000, Manuel M T Chakravarty wrote:

...

Just to complete transferring the discussion from the ephemeral hpaste to the mailing list. My response to the lack of being able to display normalised types was that GHC actually goes to considerable trouble to preserve the original (non-normalised types) for error messages and other output, as this usually makes these messages easier to understand (eg, you usually rather like String than [Char] in an error message).

That's what they always say, but IME GHC's unpredictable mixing of expanded and unexpanded form is more confusing than a straight macro-expansion would be. What are the motivating examples (ideally I'd like a mailing list thread or paper citation)? Stefan

Claus Reinke

2:26 a.m.

New subject: Monad.Reader 8: Haskell, the new C++

...

PS: And, no, you won't be able to set breakpoints in type-level programs...

but will i be able to lift type-level programs to the kind level? :-)

Stefan Monnier

6:28 p.m.

New subject: Monad.Reader 8: Haskell, the new C++

...

PS: And, no, you won't be able to set breakpoints in type-level programs...

Yet. Stefan

Don Stewart

13 Sep 13 Sep

6:12 p.m.

New subject: Monad.Reader 8: Haskell, the new C++

...

...
Better here means "better" -- a functional language on the type system, to type a functional language on the value level.

-- Don

For a taste, see Instant Insanity transliterated in this functional language:

http://hpaste.org/2689

NB: it took me 5 minutes, and that was my first piece of coding ever with Type families

Wow. Great work! The new age of type hackery has dawned. -- Don

Peter Verswyvelen

8:12 p.m.

New subject: Monad.Reader 8: Haskell, the new C++

This is all very cool stuff, but sometimes I wander if it isn't possible to drop the special languages for fiddling with types, and introduce just a single language which has no types, only raw data from which you can built your own "types" (as in the old days when we used macro assemblers ;-), but the language has two special keywords: static and dynamic, where code annotated with static runs in the "compiler domain", and code annotated with dynamic runs in "application domain". Of course, I don't know much about this, so this idea might be totally insane ;-) Probably this is impossible because of the halting problem or something... Pete Don Stewart wrote:

...

...
...
Better here means "better" -- a functional language on the type system, to type a functional language on the value level.

-- Don

For a taste, see Instant Insanity transliterated in this functional language:

http://hpaste.org/2689

NB: it took me 5 minutes, and that was my first piece of coding ever with Type families

Wow. Great work!

The new age of type hackery has dawned.

-- Don _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Adrian Neumann

14 Sep 14 Sep

6:24 a.m.

New subject: Monad.Reader 8: Haskell, the new C++

-----BEGIN PGP SIGNED MESSAGE----- Hash: RIPEMD160 I heard only rumors, but isn't Lisp supposed to be just that? A programmable programming language? Peter Verswyvelen schrieb:

...

This is all very cool stuff, but sometimes I wander if it isn't possible to drop the special languages for fiddling with types, and introduce just a single language which has no types, only raw data from which you can built your own "types" (as in the old days when we used macro assemblers ;-), but the language has two special keywords: static and dynamic, where code annotated with static runs in the "compiler domain", and code annotated with dynamic runs in "application domain". Of course, I don't know much about this, so this idea might be totally insane ;-) Probably this is impossible because of the halting problem or something...

Pete

Don Stewart wrote:

...
...
...
Better here means "better" -- a functional language on the type system, to type a functional language on the value level.

-- Don

For a taste, see Instant Insanity transliterated in this functional language:

http://hpaste.org/2689

NB: it took me 5 minutes, and that was my first piece of coding ever with Type families

Wow. Great work! The new age of type hackery has dawned.

-- Don _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.7 (MingW32) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQFG6ikc11V8mqIQMRsRA+PzAKCN0bC6lv8p9WEwJkJrcczktIdKGACfUdkt 0QBGlmgwfYrKS6lKEwQihkc= =31jo -----END PGP SIGNATURE-----

Peter Verswyvelen

7:55 p.m.

New subject: Monad.Reader 8: Haskell, the new C++

I'm not sure, I don't know LISP in detail, but as far as I know, LISP is a fully dynamic language. I actually meant a static language where you build your own strong types using the language itself. On the micro level, the language only knows abouts bits and bytes without semantics, just like assembler, no types at all. But the language allows you to build whatever "type" or "semantics" you want from scratch, by providing a keyword that forces certain part of the program to be evaluated at compile time. A bit like macros, but written in the same language. Although not exactly the same, the Digital Mars D language has a "static if (p) { q }" statement, where p must evaluate to a constant expression at compile time, otherwise the compiler gives an error/warning (I'm not sure, haven't tried it yet). You can do that in C++ (using templates) and Haskell (using types) but these are actually mini-sub-languages. Probably giving control to the programmer of how type-checking should be coded bypasses the advantages of strong typing, so this is most likely a dumb idea... Anyway, I should not mention these ideas, I'm just a programmer, not a computer scientist ;-) Peter Adrian Neumann wrote:

...

-----BEGIN PGP SIGNED MESSAGE----- Hash: RIPEMD160

I heard only rumors, but isn't Lisp supposed to be just that? A programmable programming language?

Peter Verswyvelen schrieb:

...
This is all very cool stuff, but sometimes I wander if it isn't possible to drop the special languages for fiddling with types, and introduce just a single language which has no types, only raw data from which you can built your own "types" (as in the old days when we used macro assemblers ;-), but the language has two special keywords: static and dynamic, where code annotated with static runs in the "compiler domain", and code annotated with dynamic runs in "application domain". Of course, I don't know much about this, so this idea might be totally insane ;-) Probably this is impossible because of the halting problem or something...

Pete

Don Stewart wrote:

...
...
...
Better here means "better" -- a functional language on the type system, to type a functional language on the value level.

-- Don

For a taste, see Instant Insanity transliterated in this functional language:

http://hpaste.org/2689

NB: it took me 5 minutes, and that was my first piece of coding ever with Type families

Wow. Great work! The new age of type hackery has dawned.

-- Don _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.7 (MingW32) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFG6ikc11V8mqIQMRsRA+PzAKCN0bC6lv8p9WEwJkJrcczktIdKGACfUdkt 0QBGlmgwfYrKS6lKEwQihkc= =31jo -----END PGP SIGNATURE----- _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Toby Allsopp

8:44 p.m.

New subject: Monad.Reader 8: Haskell, the new C++

Peter Verswyvelen writes:

...

I'm not sure, I don't know LISP in detail, but as far as I know, LISP is a fully dynamic language.

I actually meant a static language where you build your own strong types using the language itself. [...]

You might be interested in the Qi language[1]. Qi is implemented on top of Common Lisp using macros (and probably other things) and provides (optional) static type checking as well as various functional programming features (pattern matching, partial function application, etc.) The implementation, including all of the type checking, is in Common Lisp and runs during compilation (well, technically at macro-expansion time.) A Qi program is just a Common Lisp program that can choose to use the features provided by these macros. Regards, Toby. Footnotes: [1] http://www.lambdassociates.org/aboutqi.htm

Bill Wood

15 Sep 15 Sep

2:45 a.m.

New subject: Monad.Reader 8: Haskell, the new C++

On Fri, 2007-09-14 at 21:55 +0200, Peter Verswyvelen wrote:

...

I'm not sure, I don't know LISP in detail, but as far as I know, LISP is a fully dynamic language.

I actually meant a static language where you build your own strong types using the language itself. On the micro level, the language only knows abouts bits and bytes without semantics, just like assembler, no types at all. But the language allows you to build whatever "type" or "semantics" you want from scratch, by providing a keyword that forces certain part of the program to be evaluated at compile time. A bit like macros, but written in the same language. Although not exactly the same, the Digital Mars D language has a "static if (p) { q }" statement, where p must evaluate to a constant expression at compile time, otherwise the compiler gives an error/warning (I'm not sure, haven't tried it yet). You can do that in C++ (using templates) and Haskell (using types) but these are actually mini-sub-languages. Probably giving control to the programmer of how type-checking should be coded bypasses the advantages of strong typing, so this is most likely a dumb idea...

You might find Forth interesting/entertaining. After implementing versions of Dijkstra's guarded if and do constructs using the same mechanisms that were used to implement the "native" control structures I decided that Forth was the closest thing to a genuine extensible language that I had ever worked with. -- Bill Wood

Derek Elkins

13 Sep 13 Sep

9:01 p.m.

New subject: Monad.Reader 8: Haskell, the new C++

On Thu, 2007-09-13 at 11:12 -0700, Don Stewart wrote:

...

...
...
Better here means "better" -- a functional language on the type system, to type a functional language on the value level.

-- Don

For a taste, see Instant Insanity transliterated in this functional language:

http://hpaste.org/2689

NB: it took me 5 minutes, and that was my first piece of coding ever with Type families

Wow. Great work!

The new age of type hackery has dawned.

Is the type level functional language non-strict? (Is there a flag that will allow non-terminating associated type programs?)

Manuel M T Chakravarty

14 Sep 14 Sep

1:25 a.m.

New subject: Monad.Reader 8: Haskell, the new C++

Derek Elkins wrote,

...

On Thu, 2007-09-13 at 11:12 -0700, Don Stewart wrote:

...
...
...
Better here means "better" -- a functional language on the type system, to type a functional language on the value level.

-- Don For a taste, see Instant Insanity transliterated in this functional language:

http://hpaste.org/2689

NB: it took me 5 minutes, and that was my first piece of coding ever with Type families Wow. Great work!

The new age of type hackery has dawned.

Is the type level functional language non-strict? (Is there a flag that will allow non-terminating associated type programs?)

The associated type theory is only concerned with terminating (aka strongly normalising) sets of type instances. For a strongly normalising calculus, it does not matter whether you use eager or non-strict evaluation. However, there is of course a flag to diable the check for termination and to give up on decidable type checking.[1] It's the same flag as for type classes: -fallow-undecidable-instances (Equations of type families, or type-level functions, are introduced with the keywords "type instance", so the option name still makes sense.) FWIW, the evaluation strategy in this case is right now fairly eager, but it is a little hard to characterise. If the application of a type family needs to be normalised to proceed with unification, eg, [a] ~ F (G Int) then F (G Int) will be eagerly evaluated (ie, first G Int, and then (F <result of G Int>). However, type-level data constructors (ie, type constructors are non-strict); eg, [a] ~ [F Int] will result in the substitution [F Int/a]. And you can use cyclic bindings: a ~ F a However, they must have a finite solution, as we still only admit finite types; eg, the following definition of F would be fine: type family F a type instance F a = Int but type family F a type instance F a = [a] will give you one of these "cannot construct infinite type: a ~ [a]" messages. This makes it a bit like Id/pH's lenient evaluation. Manuel [1] This is GHC after all, it tries to gently nudge you in the right direction, but if you insist, it happily let's you drill arbitrarily large holes in your foot.

Albert Y. C. Lai

12 Sep 12 Sep

10:06 p.m.

New subject: Monad.Reader 8: Haskell, the new C++

ok wrote:

...

So we have

C++ : imperative language whose type system is a Turing-complete functional language (with rather twisted syntax)

Haskell: functional language whose type system is a Turing- complete logic programming language (with rather twisted syntax)

They also have twisted semantics.

...

I've been told that functional dependencies are old hat and there is now something better. I suspect that "better" here means "worse".

Lattice duality, Galois connections, functor adjunctions, etc., have taught me that better is always equivalent to worse.

Stefan Holdermans

13 Sep 13 Sep

4:27 a.m.

New subject: Monad.Reader 8: Haskell, the new C++

...

C++ : imperative language whose type system is a Turing-complete functional language (with rather twisted syntax)

Haskell: functional language whose type system is a Turing- complete logic programming language (with rather twisted syntax)

Since not all Turing machines halt, and since the halting problem is undecidable, this means not only that some Haskell programs will make the type checker loop forever, but that there is no possible meta- checker that could warn us when that would happen.

Do not forget that both functional dependencies and associated types come with syntactic restrictions that are there just to "tame" the Turing completeness, i.e., to guarantee that type checking will actually terminate. (I do agree that these restrictions, for functional dependencies anyway, can be thought of as twisted in their own right, but then again, there's no such thing as a free lunch.) Admittedly, it's my experience that whenever one wants to do something interesting (and here I mean "interesting" in a way that you would probably label as "rather twisted" ;-)), one has to bypass these restrictions (and, hence, allow for potentially undecidable instances). Now, I haven't really worked with associated types (or, for that matter, associated type synonyms), but my hope is that, when using those, turning off the checks is needed less often. We'll see. Another option would be not to care that much about looping type checkers: when it loops, you'll probabely notice it quite soon already :-). That said, that would not be the option I'd pick though: being restricted to, say, structural recursion on the type-level could well cause your type-level programs to be better organised. Cheers, Stefan

ok

10:42 p.m.

New subject: Monad.Reader 8: Haskell, the new C++

I wrote:

...

...
Since not all Turing machines halt, and since the halting problem is undecidable, this means not only that some Haskell programs will make the type checker loop forever, but that there is no possible meta- checker that could warn us when that would happen.

On 13 Sep 2007, at 4:27 pm, Stefan Holdermans wrote:

...

Do not forget that both functional dependencies and associated types come with syntactic restrictions that are there just to "tame" the Turing completeness, i.e., to guarantee that type checking will actually terminate.

I don't know anything about associated types, so can't comment on those. But on the subject of functional dependencies, you and the author of the article in Monad.Reader 8 *cannot* both be right, because the whole point of that article is to explain how to program in the type system, using, amongst other things, conditionals and recursion, in such a way that a Turing machine can surely be simulated. If there is some restriction to guarantee termination, then those techniques can't work.

...

Admittedly, it's my experience that whenever one wants to do something interesting (and here I mean "interesting" in a way that you would probably label as "rather twisted" ;-)), one has to bypass these restrictions (and, hence, allow for potentially undecidable instances).

Ah, now we have it. To quote Conrad Parker: This tutorial uses the Haskell98 type system extended with multi-parameter typeclasses and undecidable instances. We need to enable some GHC extensions to play with this type- hackery: $ ghci -fglasgow-exts -fallow-undecidable-instances That is the combination I'm talking about.

...

Now, I haven't really worked with associated types (or, for that matter, associated type synonyms), but my hope is that, when using those, turning off the checks is needed less often. We'll see.

If you hope that, then we probably agree more than you might think. My point is that the combination exists and is being explained so that people can use it, and that the result is comparable in C++. (Imagine Dame Edna Everage saying "I mean that in a loving way, possums.")

Thomas Schilling

11:05 p.m.

New subject: Monad.Reader 8: Haskell, the new C++

On Fri, 2007-09-14 at 10:42 +1200, ok wrote:

...

I wrote:

...
...
Since not all Turing machines halt, and since the halting problem is undecidable, this means not only that some Haskell programs will make the type checker loop forever, but that there is no possible meta- checker that could warn us when that would happen.

On 13 Sep 2007, at 4:27 pm, Stefan Holdermans wrote:

...
Do not forget that both functional dependencies and associated types come with syntactic restrictions that are there just to "tame" the Turing completeness, i.e., to guarantee that type checking will actually terminate.

I don't know anything about associated types, so can't comment on those. But on the subject of functional dependencies, you and the author of the article in Monad.Reader 8 *cannot* both be right, because the whole point of that article is to explain how to program in the type system, using, amongst other things, conditionals and recursion, in such a way that a Turing machine can surely be simulated. If there is some restriction to guarantee termination, then those techniques can't work.

...
...
Admittedly, it's my experience that whenever one wants to do something interesting (and here I mean "interesting" in a way that you would probably label as "rather twisted" ;-)), one has to bypass these restrictions (and, hence, allow for potentially undecidable instances).

Ah, now we have it. To quote Conrad Parker: This tutorial uses the Haskell98 type system extended with multi-parameter typeclasses and undecidable instances. We need to enable some GHC extensions to play with this type- hackery: $ ghci -fglasgow-exts -fallow-undecidable-instances

That is the combination I'm talking about.

...
Now, I haven't really worked with associated types (or, for that matter, associated type synonyms), but my hope is that, when using those, turning off the checks is needed less often. We'll see.

If you hope that, then we probably agree more than you might think. My point is that the combination exists and is being explained so that people can use it, and that the result is comparable in C++. (Imagine Dame Edna Everage saying "I mean that in a loving way, possums.")

The type system doesn't help you avoid writing non-terminating programs, so i see no problem with it being possible giving programmers the power to express and check more complex properties of their programs -- as long as type-checking remains sound. From a practical standpoint, non-terminating type checks are just as much a bug as non-terminating library functions. Type systems need more thought anyways, so why not make sure it's terminating, too? The other extreme is to use dependent types everywhere, but this has a bit more drastic consequences to the accessibility and practicality of the language. I don't think this will become a mainstream tool any time soon, but it may turn out to be very valuable to library authors. We also shouldn't forget that this is a brand-new feature and requires proper evaluation; how better could this be achieved than by having it included as an optional feature in a mature and well-used compiler? I am glad that Haskellers try to integrate theory and practice that nicely. / Thomas

Thomas Conway

14 Sep 14 Sep

1:57 a.m.

New subject: Monad.Reader 8: Haskell, the new C++

On 9/14/07, Thomas Schilling wrote:

...

The type system doesn't help you avoid writing non-terminating programs, so i see no problem with it being possible giving programmers the power to express and check more complex properties of their programs -- as long as type-checking remains sound. From a practical standpoint, non-terminating type checks are just as much a bug as non-terminating library functions. Type systems need more thought anyways, so why not make sure it's terminating, too? The other extreme is to use dependent types everywhere, but this has a bit more drastic consequences to the accessibility and practicality of the language.

While I love all the exceedingly cool type hackery, I also like the compiler to terminate. Some people in this forum may be old enough to remember Turbo Prolog. It did mode inference (i.e. data-flow analysis) on programs, but unfortunately it didn't always terminate. So what you got was a hung compiler, leaving you to guess what it was about your [quite possibly correct] program that caused the analysis to loop. With C++ templates, the problem is addressed by having a limit to the depth of the "call stack" for template evaluation. I recall with Forte 5, there was no flag to let you increase the depth, so at one point we had to do something like if (0) { // Horrible nasty expression to force the evaluation of some of the // the lower parts of the template stack } This works because (at least in Forte 5, and probably most implementations) template instantiations are hash-consed. I would *much* rather have a simpler type system, than a compiler which might not terminate. cheers, T. -- Thomas Conway drtomc@gmail.com Silence is the perfectest herald of joy: I were but little happy, if I could say how much.

PR Stanley

11 Sep 11 Sep

11:46 p.m.

Let me get this right, are you saying it's unsafe when it returns an error? Paul At 00:40 12/09/2007, you wrote:

...

byorgey:

...
On 9/11/07, PR Stanley <[1]prstanley@ntlworld.com> wrote:

Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. Any ideas? Thanks, Paul

If for some reason you want a version that does return an error in that situation, you could do something like the following:

take' n _ | (n <= 0) = [] take' n [] | (n > 0) = error "take': list too short" | otherwise = [] take' n (x:xs) = x : take' (n-1) xs

And we'd call it unsafeTake, just like unsafeFromJust and unsafeTail :-)

-- Don

Don Stewart

11:49 p.m.

prstanley:

...

Let me get this right, are you saying it's unsafe when it returns an error?

Partial functions may crash your program, so that's unsafe by some definitions, yep. We have tools that analyse programs for such bugs, in fact (Neil's `catch' program). -- Don

John Meacham

11:45 p.m.

On Tue, Sep 11, 2007 at 07:38:18PM -0400, Brent Yorgey wrote:

...

On 9/11/07, PR Stanley wrote:

...
Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. Any ideas? Thanks, Paul

If for some reason you want a version that does return an error in that situation, you could do something like the following:

take' n _ | (n <= 0) = [] take' n [] | (n > 0) = error "take': list too short" | otherwise = [] take' n (x:xs) = x : take' (n-1) xs

you could also do something like take' n xs = take n (xs ++ error "I want more!") John -- John Meacham - ⑆repetae.net⑆john⑈

Conor McBride

12 Sep 12 Sep

9:03 a.m.

Hi folks On 12 Sep 2007, at 00:38, Brent Yorgey wrote:

...

On 9/11/07, PR Stanley wrote: Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error.

[..]

...

If for some reason you want a version that does return an error in that situation, you could do something like the following:

take' n _ | (n <= 0) = [] take' n [] | (n > 0) = error "take': list too short" | otherwise = [] take' n (x:xs) = x : take' (n-1) xs

I'm not sure why you'd want that, though. The standard implementation gracefully handles all inputs, and usually turns out to be what you want.

There are two sides to this form of "grace", though. I'll grant you, it's quite hard to pull off a successful fraud without a degree of aplomb. I always hope that key invariants and hygiene conditions can be built into the static semantics of programs, but where that's impractical somehow, I prefer if the dynamic behaviour makes it as easy as possible to assign the blame for errors. In such circumstances, I'd like operations to complain about bogus input, rather than producing bogus output. These GIGO problems do bite in real life. I spent a long time finding a bug in somebody else's typechecker which boiled down to the silly mistake of zipping the wrong lists together. The right lists were guaranteed to match in length, but there was no reason for the wrong lists to do so. Problem: unless you were doing fairly wacky stuff, they both happened to have length zero. Once weirder things arrived, the discrepancies showed up and the truncations started happening, causing well-formed but ill-typed expressions to be generated by and propagated around the kernel of the system, which eventually choked in some essentially random place. We had many suspects before we found the culprit. If the programmer had used a version of zip which bombed in off-diagonal cases, we'd have been straight there. So I might very well consider having more than one version of take around, depending on my requirements for its use. I might even consider the more informative function which also returns the length of the shortfall. In a dependently typed setting, I wouldn't write take and drop: I'd equip lists with a view incorporating both, guaranteeing the length invariants and that the sublists actually append to the input. But where shame is unattainable, blame is really quite important. All the best Conor

ChrisK

10:44 a.m.

Conor McBride wrote:

...

Hi folks

On 12 Sep 2007, at 00:38, Brent Yorgey wrote:

...
On 9/11/07, PR Stanley wrote: Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error.

[..]

...
If for some reason you want a version that does return an error in that situation, you could do something like the following:

take' n _ | (n <= 0) = [] take' n [] | (n > 0) = error "take': list too short" | otherwise = [] take' n (x:xs) = x : take' (n-1) xs

I'm not sure why you'd want that, though. The standard implementation gracefully handles all inputs, and usually turns out to be what you want.

There are two sides to this form of "grace", though. I'll grant you, it's quite hard to pull off a successful fraud without a degree of aplomb.

I always hope that key invariants and hygiene conditions can be built into the static semantics of programs, but where that's impractical somehow, I prefer if the dynamic behaviour makes it as easy as possible to assign the blame for errors. In such circumstances, I'd like operations to complain about bogus input, rather than producing bogus output.

Then you want a runtime assertion checking error helpful Data.List replacement. Could you use Control.Exception.assert and make a wrapper for Data.List? http://www.haskell.org/ghc/docs/latest/html/users_guide/sec-assertions.html

Conor McBride

3:43 p.m.

Hi On 12 Sep 2007, at 11:44, ChrisK wrote:

...

Conor McBride wrote:

...
I'd like operations to complain about bogus input, rather than producing bogus output.

Then you want a runtime assertion checking error helpful Data.List replacement.

Could you use Control.Exception.assert and make a wrapper for Data.List?

http://www.haskell.org/ghc/docs/latest/html/users_guide/sec- assertions.html

Hmmm. It might be quite annoying to make it a wrapper if it's just a question of appealing to error rather than returning dummy values in failure cases. Defining the domain of a function can be quite like defining the function itself. Also, sometimes there can be problems arriving at a Bool. For example, zipping colists is a productive coprogram, and it can raise errors in off-diagonal cases, but you can't compute in advance whether you're on the diagonal. A more serious point is that in some cases we might want take to underapproximate, or zip to truncate (or tail [] = [] ?). I don't think there's always a clear "library" choice here. I tend to be pragmatic about it. I was just pointing out that it does sometimes make sense to use less defined functions when one has a more specific domain in mind. I'm usually happy to write the fussy variants myself, if I'm that agitated. Funny old world Conor

Neil Mitchell

4:01 p.m.

...

A more serious point is that in some cases we might want take to underapproximate, or zip to truncate (or tail [] = [] ?). I don't think there's always a clear "library" choice here.

I have a zipWithEq function I often use, which crashes if the zip'd lists aren't equal. I also have tailSafe which does the tailSafe [] = [] behaviour. I created a hackage package "safe" for the tailSafe function and others, http://www-users.cs.york.ac.uk/~ndm/safe/ . If anyone wants to extend that with deliberately unsafe functions, such as zipWithUnsafe, zipUnsafe, takeUnsafe etc, I'd be happy to accept a patch. If not, I'll probably do it myself at some point in the (potentially distant) future. Thanks Neil

Jules Bean

13 Sep 13 Sep

8:43 a.m.

Neil Mitchell wrote:

...

Hi

...
A more serious point is that in some cases we might want take to underapproximate, or zip to truncate (or tail [] = [] ?). I don't think there's always a clear "library" choice here.

I have a zipWithEq function I often use, which crashes if the zip'd lists aren't equal. I also have tailSafe which does the tailSafe [] = [] behaviour. I created a hackage package "safe" for the tailSafe function and others, http://www-users.cs.york.ac.uk/~ndm/safe/ . If anyone wants to extend that with deliberately unsafe functions, such as zipWithUnsafe, zipUnsafe, takeUnsafe etc, I'd be happy to accept a patch. If not, I'll probably do it myself at some point in the (potentially distant) future.

Of course we have tailSafe in the standard library (if I correctly understand what you mean) as "drop 1" and headSafe as "take 1". I've rather got used to the exact details of head/tail, take/drop and zip but I agree it's a bit arbitrary: counterintuitive until you learn which is which and which is what. Although I appluad the semantics of the safe package, I'm not delighted with the idea of replacing our concise elegant standard library names with uglyAndRatherLongCamelCaseNamesThatCouldBePerlOrEvenJava though. Conciseness of expression is a virtue. Jules

Neil Mitchell

8:50 a.m.

...

Although I appluad the semantics of the safe package, I'm not delighted with the idea of replacing our concise elegant standard library names with uglyAndRatherLongCamelCaseNamesThatCouldBePerlOrEvenJava though. Conciseness of expression is a virtue.

They aren't that long - merely an extra 4 characters over the standard one to indicate what the specific semantics are. If you can think of better names, then I'm happy to make use of them. Thanks Neil

Jules Bean

8:56 a.m.

Neil Mitchell wrote:

...

Hi

...
Although I appluad the semantics of the safe package, I'm not delighted with the idea of replacing our concise elegant standard library names with uglyAndRatherLongCamelCaseNamesThatCouldBePerlOrEvenJava though. Conciseness of expression is a virtue.

They aren't that long - merely an extra 4 characters over the standard one to indicate what the specific semantics are. If you can think of better names, then I'm happy to make use of them.

No, they're not, and it wasn't intended as a slight against your naming choice. I don't have a better suggestion. The problem I was really trying to point at, but didn't express at all well, was that a proliferation of similar functions with slightly different names (like Conor's four versions of zipWith) doesn't make a very elegant library API. It's nicer to settle on a smaller number of primitives. I don't actually have a solution that I think is "good" for the head/tail/take/drop issue :-( Jules

Ketil Malde

9:47 a.m.

On Thu, 2007-09-13 at 09:56 +0100, Jules Bean wrote:

...

Neil Mitchell wrote:

...
Hi

...
Although I appluad the semantics of the safe package, I'm not delighted with the idea of replacing our concise elegant standard library names with uglyAndRatherLongCamelCaseNamesThatCouldBePerlOrEvenJava though. Conciseness of expression is a virtue.

They aren't that long - merely an extra 4 characters over the standard one to indicate what the specific semantics are. If you can think of better names, then I'm happy to make use of them.

No, they're not, and it wasn't intended as a slight against your naming choice. I don't have a better suggestion.

Isn't there sort of a tradition for 'unsafe' to mean dangerous territory, beyond mere domain limitations for functions, so to call this 'safe' may be a bit misleading? Similarly, I expect foo and foo' to be equivalent, except for strictness properties, but perhaps an underscore could be used for slightly different behaviors (interpretations, as it were)? "tail_" or "zip_", anyone? -k

Neil Mitchell

10:03 a.m.

...

Similarly, I expect foo and foo' to be equivalent, except for strictness properties, but perhaps an underscore could be used for slightly different behaviors (interpretations, as it were)? "tail_" or "zip_", anyone?

There are 4 variants of tail: tail :: [a] -> [a] -- normal tailDef :: [a] -> [a] -> [a] -- returns the first argument on [] tailMay :: [a] -> Maybe [a] -- returns a Nothing tailNote :: String -> [a] -> [a] -- crashes, but with a helpful message tailSafe :: [a] -> [a] -- returns [] on [] tail_____ would not be a good name! Thanks Neil

Jeff Polakow

12:44 p.m.

Hello,

...

There are 4 variants of tail:

tail :: [a] -> [a] -- normal tailDef :: [a] -> [a] -> [a] -- returns the first argument on [] tailMay :: [a] -> Maybe [a] -- returns a Nothing tailNote :: String -> [a] -> [a] -- crashes, but with a helpful message tailSafe :: [a] -> [a] -- returns [] on []

Is there a reason for not having tailM :: Monad m => [a] -> m [a] which, at least for me, is much more useful? -Jeff --- This e-mail may contain confidential and/or privileged information. If you are not the intended recipient (or have received this e-mail in error) please notify the sender immediately and destroy this e-mail. Any unauthorized copying, disclosure or distribution of the material in this e-mail is strictly forbidden.

Neil Mitchell

12:46 p.m.

...

Is there a reason for not having

tailM :: Monad m => [a] -> m [a]

which, at least for me, is much more useful?

No, that probably is a much more sensible choice. Patches welcome :) Thanks Neil

Jules Bean

1:02 p.m.

Jeff Polakow wrote:

...

Hello,

...
There are 4 variants of tail:

tail :: [a] -> [a] -- normal tailDef :: [a] -> [a] -> [a] -- returns the first argument on [] tailMay :: [a] -> Maybe [a] -- returns a Nothing tailNote :: String -> [a] -> [a] -- crashes, but with a helpful message tailSafe :: [a] -> [a] -- returns [] on []

Is there a reason for not having

tailM :: Monad m => [a] -> m [a]

Monads are not an (elegant, or deliberate) abstraction of failure. Jules

Lutz Donnerhacke

12:49 p.m.

* Neil Mitchell wrote:

...

There are 4 variants of tail:

tail :: [a] -> [a] -- normal tailDef :: [a] -> [a] -> [a] -- returns the first argument on [] tailMay :: [a] -> Maybe [a] -- returns a Nothing tailNote :: String -> [a] -> [a] -- crashes, but with a helpful message tailSafe :: [a] -> [a] -- returns [] on []

...

From the logical point of view tailMay is the right one. It pushes the error handling to the caller programm.

tail = fromJust . tailMay

Neil Mitchell

12:56 p.m.

...

...
From the logical point of view tailMay is the right one. It pushes the error handling to the caller programm.

tail = fromJust . tailMay

The error messages suffer: tail [] = "error: fromJust Nothing" That's why I supplied tailNote, where tailNote "foo broke its invariant!" [] gives the message "error: tail [], foo broke its invariant!" Thanks Neil

Ketil Malde

1:16 p.m.

On Thu, 2007-09-13 at 13:56 +0100, Neil Mitchell wrote:

...

...
tail = fromJust . tailMay

The error messages suffer [..] That's why I supplied tailNote

Still, given tailMay, we have: tailDef xs = maybe xs id . tailMay tailNote msg = tailDef (error msg) tailSafe = tailDef [] tail = tailNote "tail: empty list" which I suppose was Lutz's point? (My rather ugly preference is to #define tail so that an error message contains source code location.) -k

Andrew Coppin

6:13 p.m.

Jules Bean wrote:

...

I'm not delighted with the idea of replacing our concise elegant standard library names with uglyAndRatherLongCamelCaseNamesThatCouldBePerlOrEvenJava though. Conciseness of expression is a virtue.

I, on the other hand, I'm not delighted with names such as "Eq" and "Ord". (Would it be *so* hard to write "Equal" and "Ordered"?) This is one of the main things I'd have done differently if I'd designed Haskell... not that anybody is too bothered. ;-)

PR Stanley

12 Sep 12 Sep

4:08 p.m.

I quite like the argument that take is a total function and as such all its return values are from teh specificed range. I can also see the logic in take n [] = [] where n > 0 taking n from nothing, or the empty set, returns nothing! The same should apply to head and tail. head or tail of [] should be []. What does the list think? Cheers, Paul At 16:43 12/09/2007, you wrote:

...

Hi

On 12 Sep 2007, at 11:44, ChrisK wrote:

...
Conor McBride wrote:

...
I'd like operations to complain about bogus input, rather than producing bogus output.

Then you want a runtime assertion checking error helpful Data.List replacement.

Could you use Control.Exception.assert and make a wrapper for Data.List?

http://www.haskell.org/ghc/docs/latest/html/users_guide/sec- assertions.html

Hmmm. It might be quite annoying to make it a wrapper if it's just a question of appealing to error rather than returning dummy values in failure cases. Defining the domain of a function can be quite like defining the function itself. Also, sometimes there can be problems arriving at a Bool. For example, zipping colists is a productive coprogram, and it can raise errors in off-diagonal cases, but you can't compute in advance whether you're on the diagonal.

A more serious point is that in some cases we might want take to underapproximate, or zip to truncate (or tail [] = [] ?). I don't think there's always a clear "library" choice here. I tend to be pragmatic about it. I was just pointing out that it does sometimes make sense to use less defined functions when one has a more specific domain in mind. I'm usually happy to write the fussy variants myself, if I'm that agitated.

Funny old world

Conor

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Neil Mitchell

4:19 p.m.

...

The same should apply to head and tail. head or tail of [] should be [].

What does the list think?

Disagree, strongly. Its not even possible for head, since [a] -> a. Wadler's theorems for free states that if head is given an empty list the _only_ thing it can do is crash. Thanks Neil

Henning Thielemann

4:34 p.m.

On Wed, 12 Sep 2007, PR Stanley wrote:

...

I quite like the argument that take is a total function and as such all its return values are from teh specificed range. I can also see the logic in take n [] = [] where n > 0 taking n from nothing, or the empty set, returns nothing! The same should apply to head and tail. head or tail of [] should be [].

Today you can use (drop 1) which has this property. However I consider it bad style that 'tail' and 'drop' behave so differently, and that one has to write (drop 1) when in fact (tailSafe) is meant. People reading (drop 1) in a program may assume, that the programmer was a newbie, who was not aware of 'tail'.

Henning Thielemann

12:39 p.m.

On Wed, 12 Sep 2007, Conor McBride wrote:

...

Hi folks

On 12 Sep 2007, at 00:38, Brent Yorgey wrote:

...
On 9/11/07, PR Stanley wrote: Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error.

[..]

...
If for some reason you want a version that does return an error in that situation, you could do something like the following:

take' n _ | (n <= 0) = [] take' n [] | (n > 0) = error "take': list too short" | otherwise = [] take' n (x:xs) = x : take' (n-1) xs

I'm not sure why you'd want that, though. The standard implementation gracefully handles all inputs, and usually turns out to be what you want.

I always hope that key invariants and hygiene conditions can be built into the static semantics of programs, but where that's impractical somehow, I prefer if the dynamic behaviour makes it as easy as possible to assign the blame for errors. In such circumstances, I'd like operations to complain about bogus input, rather than producing bogus output.

Seconded. The List functions have some kind of "scripting language semantics" or "C semantics", that is, consume almost every input, regardless of the meaning of the output, just in order to avoid error messages. Indeed there are some usages like taking a prefix of an infinite list (zip "abc" [1..]), where the current behaviour of 'zip' is useful. However it would be better to have versions of 'zip' to support these special cases. Ideally the equal length could be expressed in types, like zipInfInf :: InfiniteList a -> InfiniteList b -> InfiniteList (a,b) zipInf :: InfiniteList a -> FiniteList n b -> FiniteList n (a,b) zip :: FiniteList n a -> FiniteList n b -> FiniteList n (a,b) , which would need dependent types.

...

These GIGO problems do bite in real life. I spent a long time finding a bug in somebody else's typechecker which boiled down to the silly mistake of zipping the wrong lists together. The right lists were guaranteed to match in length, but there was no reason for the wrong lists to do so.

I had a bug which was due to the wrong order of applications of 'filter' and 'zip'. I had two lists 'a' and 'b' of the same length, where 'b' contained a condition for filtering, then I wrote zip a (filter p b) instead of filter (p . snd) $ zip a b The wrong version was temptingly short, but it matched the wrong elements. The bug had been catched early, if 'zip' would have checked the length of its inputs.

Dan Weston

7:30 p.m.

One idiom I rely on pretty often is

...

(id &&& tail) >>> uncurry (zipWith f)

to do pairwise binary operations (though I suspect an Applicative functor might be a better way to go?). E.g. my solution for ProjectEuler problem #18 (max sum of vertical path through a triangle of integers) is:

...

f = curry $ second ((id &&& tail) >>> uncurry (zipWith max)) >>> uncurry (zipWith (+) )

zeroes = repeat 0 maxTotal = foldr f zeroes

Key to this idiom is that zipWith stops after the shortest element. Otherwise, I'd need an extra init function and have to test for empty lists. So there is at least one good reason for the way zipWith works. Dan Weston Conor McBride wrote:

...

Hi folks

On 12 Sep 2007, at 00:38, Brent Yorgey wrote:

...
On 9/11/07, PR Stanley wrote: Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error.

[..]

...
If for some reason you want a version that does return an error in that situation, you could do something like the following:

take' n _ | (n <= 0) = [] take' n [] | (n > 0) = error "take': list too short" | otherwise = [] take' n (x:xs) = x : take' (n-1) xs

I'm not sure why you'd want that, though. The standard implementation gracefully handles all inputs, and usually turns out to be what you want.

There are two sides to this form of "grace", though. I'll grant you, it's quite hard to pull off a successful fraud without a degree of aplomb.

I always hope that key invariants and hygiene conditions can be built into the static semantics of programs, but where that's impractical somehow, I prefer if the dynamic behaviour makes it as easy as possible to assign the blame for errors. In such circumstances, I'd like operations to complain about bogus input, rather than producing bogus output.

These GIGO problems do bite in real life. I spent a long time finding a bug in somebody else's typechecker which boiled down to the silly mistake of zipping the wrong lists together. The right lists were guaranteed to match in length, but there was no reason for the wrong lists to do so. Problem: unless you were doing fairly wacky stuff, they both happened to have length zero. Once weirder things arrived, the discrepancies showed up and the truncations started happening, causing well-formed but ill-typed expressions to be generated by and propagated around the kernel of the system, which eventually choked in some essentially random place. We had many suspects before we found the culprit. If the programmer had used a version of zip which bombed in off-diagonal cases, we'd have been straight there.

So I might very well consider having more than one version of take around, depending on my requirements for its use. I might even consider the more informative function which also returns the length of the shortfall. In a dependently typed setting, I wouldn't write take and drop: I'd equip lists with a view incorporating both, guaranteeing the length invariants and that the sublists actually append to the input. But where shame is unattainable, blame is really quite important.

All the best

Conor

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

rahn＠ira.uka.de

8:08 a.m.

...

take 1000 [1..3] still yields [1,2,3]

You can think about take n as: Take as much as possible, but at most n elements. This behavior has some nice properties as turned out by others, but there are some pitfalls. We have length . take n /= const n in general, instead only length . take n `elem` map const [0..n] holds. Therefore head . length n is unsafe for all n, even strict positive ones. Moreover, it is easy to produce tricky code. Assume you want to know, whether the prefixes of length k are equal and write pref_eq k xs ys = take k xs == take k ys This seems to be a straightforward implementation with good properties. Now play a bit with it: Prelude> pref_eq 3 "ab" "abc" False Prelude> pref_eq 3 "ab" "ab" True Prelude> map (pref_eq 3 "ab") $ Data.List.inits "abc" [False,False,True,False] Uhh, this is not what everybody expects at first glance. In particular, if pref_eq k xs ys == False then *not* necessarily pref_eq k xs (init ys) == False. As always, quickCheck is your friend to assure (or reject) such a property. /BR

ok

10:27 p.m.

On 12 Sep 2007, at 8:08 pm, rahn@ira.uka.de wrote:

...

...
take 1000 [1..3] still yields [1,2,3]

You can think about take n as: Take as much as possible, but at most n elements. This behavior has some nice properties as turned out by others, but there are some pitfalls.

One of the very nice properties is this: for all n >= 0, m >= 0 take m . take n = take (m+n) drop m . drop n = drop (m+n) And another is this: for all xs, n >= 0 take n xs ++ drop n xs == xs

...

length . take n /= const n

in general, instead only

length . take n `elem` map const [0..n]

What we have is for all xs, n >= 0 n <= length xs => length (take n xs) == n Suppose we had the "unsafe" take. Would we then have length . take n == const n? NO! For some xs, (length . take n) xs would be bottom, while (const n) xs would be n. As far as I can see, the strongest statement about length that unsafeTake would satisfy is for all xs, n >= 0 n <= length xs => length (unsafeTake n xs) == n which is, mutatis mutandis, the SAME law that applies to the `take` we already have.

...

Therefore head . length n is unsafe for all n, even strict positive ones.

...

Moreover, it is easy to produce tricky code. Assume you want to know, whether the prefixes of length k are equal and write

pref_eq k xs ys = take k xs == take k ys

This seems to be a straightforward implementation with good properties. Actually, no, at least not if implemented naively. (I wonder just how clever GHC is with this code? I can't check at the moment. After heroic efforts by my sysadmin, I was finally able to install the binary release of GHC 6.6.1, but (a) it assumes that gcc accepts a -fwrapv flag, which gcc 3.3.2 (TWW) does not accept, and (b) after patching

I'm assuming that should have been (head . take n). The thing is that (head . take n) fails when and only when (head . unsafeTake n) fails; the only difference is which function reports the error. that, gcc still chokes on the output of GHC.) The obvious question is what pref_eq k xs ys *should* do when xs or ys is not at least k long. Does it mean "I believe xs and ys are at least k long: if they are, check their prefixes, if they aren't, raise an error" or does it mean "xs and ys are at least k long and their prefixes of length k are equal"?

...

Uhh, this is not what everybody expects at first glance. In particular, if

pref_eq k xs ys == False

then *not* necessarily

pref_eq k xs (init ys) == False.

As always, quickCheck is your friend to assure (or reject) such a property.

That is certainly so, but the fundamental issue in this example is not what take does, but "don't leap into coding a function before you know what it means". We've now seen three readings of what pref_eq means. In particular, pref_eq k xs ys = unsafeTake k xs == unsafeTake k ys would NOT satisfy the law that pref_eq k xs ys == False => pref_eq k xs (init ys) == False because pref_eq 2 [1,2] [1,3] == False but pref_eq 2 [1,2] [1] => undefined So "fixing" take would not, in this case, produce the desired behaviour.

rahn＠ira.uka.de

13 Sep 13 Sep

7:32 a.m.

...

...
pref_eq k xs ys = take k xs == take k ys

...

...
This seems to be a straightforward implementation with good properties.

...

Actually, no, at least not if implemented naively.

I choosed this example, since I stumbled on this question last week. Reputable mathematicians doing "combinatorics on words" are using exactly this definition! (Karhumäki, Harju) There are others (Holub), that use the (to the computer scientist) nicer(?) pref_eq 0 _ _ = True pref_eq _ _ [] = False pref_eq _ [] _ = False pref_eq k (x:xs) (y:ys) = x == y && pref_eq (k-1) xs ys And as you guess it, there are lemmata (and probably theorems), that hold for one of the definitions only... Later, the mathematicians agree upton to call the first version "pref_eq" and the second "pref_eq_proper". And yes, you are right, just to change the behavior of take would not solve this issue. My topic was really more like

...

"don't leap into coding a function before you know what it means"

as you pointed out with nice words :-) This is not the main topic of the thread (is this true?) but we are in a cafe, so from time to time one adds some cents... /BR

6507

Age (days ago)

6511

Last active (days ago)

List overview

Download

58 comments

32 participants

participants (32)

Aaron Denney
Adrian Neumann
Albert Y. C. Lai
Andrew Coppin
Bill Wood
Brent Yorgey
ChrisK
Claus Reinke
Conor McBride
Dan Weston
Derek Elkins
Don Stewart
Henning Thielemann
Jeff Polakow
John Meacham
Jules Bean
Ketil Malde
Lutz Donnerhacke
Manuel M T Chakravarty
Neil Mitchell
ok
Pepe Iborra
Peter Verswyvelen
PR Stanley
rahn＠ira.uka.de
Stefan Holdermans
Stefan Monnier
Stefan O'Rear
Thomas Conway
Thomas Schilling
Tim Chevalier
Toby Allsopp