Re: [Haskell-cafe] Hackage 2 now available for beta testing
] Contributing to the development === The code is on github and we welcome pull requests. There are open tickets describing existing bugs and features that we want or that are in need of improvement. Help on any of these would be greatly appreciated. There is some developer and user documentation on the github wiki, including a quick guide to getting your own server instance up and running. You can ask questions on the cabal-devel mailing list or on IRC in the #hackage channel on freenode. [code]: https://github.com/haskell/hackage-server [4] [github wiki]: https://github.com/haskell/hackage-server/wiki [7] [cabal-devel]: http://www.haskell.org/mailman/listinfo/cabal-devel [8] -- Andreas Abel Du bist der geliebte Mensch. Theoretical Computer Science, University of Munich http://www.tcs.informatik.uni-muenchen.de/~abel/ Links: -- [1] http://beta.hackage.haskell.org/ [2] http://industry.haskell.org/ [3] https://github.com/haskell/hackage-server/issues [4] https://github.com/haskell/hackage-server [5] http://hackage.haskell.org/packages/archive [6] http://beta.hackage.haskell.org/new-features [7] https://github.com/haskell/hackage-server/wiki [8] http://www.haskell.org/mailman/listinfo/cabal-devel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: New syntax for Haskell
+1 Cucumber seems to be great if you mainly want to read your code over the telephone, distribute it via national radio broadcast, or dictate it to your secretary or your voice recognition software. You can program thus without having to use you fingers. You can lie on your back on your sofa, close your eyes, and utter your programs... We could have blind Haskell/Cucumber programming contests... Tons of new possiblilities... Strongly support this proposal. ;-) Andreas On 2013-09-10 22:57, Artyom Kazak wrote: On Wed, 11 Sep 2013 00:20:26 +0400, Thiago Negri evoh...@gmail.com wrote: I hope these jokes do not cause people to be afraid to post new ideas. Agreed. I would also like to clarify that my message was much more a joke on the incomprehensibility of legal acts than on the original proposal. By the way, I am pretty impressed with this piece of Cucumber description/code: Scenario: Mislav creates a valid task with an upload When I go to the Awesome Ruby Yahh task list page of the Ruby Rockstars project When I follow + Add Task And I fill in Task title with Ohhh upload And I follow Attachment When I attach the file features/support/sample_files/dragon.jpg to upload_file And I press Add Task And I wait for 1 second And I should see Ohhh upload as a task name I was much more sceptical when I had only seen the example in Niklas's message. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe [1] -- Andreas Abel Du bist der geliebte Mensch. Theoretical Computer Science, University of Munich http://www.tcs.informatik.uni-muenchen.de/~abel/ Links: -- [1] http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Some philosophy (Was: Alternative name for return)
On 09.08.2013 17:44, Jerzy Karczmarczuk wrote: Indiscrete Thoughts by Gian-Carlo Rota, published by Birkhäuser in 1997. Available on the Web. For download or to buy? [This looks very interesting...] -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Alternative name for return
On 06.08.2013 10:46, Adam Gundry wrote:
On 06/08/13 06:14, J. Stutterheim wrote:
Suppose we now have the opportunity to change the name of the
`return` function in Monad, what would be a better name for it?
(for some definition of better)
Rather than proposing a different name, I'm going to challenge the
premise of your question. Perhaps it would be better if `return` had no
name at all. Consider the following:
return f `ap` s `ap` t
f $ s * t
do { sv - s
; tv - t
; return (f sv tv) }
Indeed, I wished the 0-ary case would be more alike to the unary and
binary case, cf.
return f0
f1 $ a1
f2 $ a1 * a2
What is needed is a nice syntax for idiom brackets.
These are all different ways of spelling
f s t
plus the necessary applicative or monadic bureaucracy. But why couldn't
we write just the plain application, and let the type system deal with
the plumbing of effects?
I would not think this is practically possible. For instance, if
f :: a - b - c
then it could be a binary function or a unary function in the context
monad reading from a, thus, application
f x
is ambiguous or too sensitive, especially with type inference.
I realise that this may be too open a research area for your project...
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Non-recursive let
On 26.07.13 6:44 PM, Andreas Abel wrote: headers0 - M.fromList $ do forM fields_header $ \ (n, fld) - do (n,) $ reflect $ fld ast Ah, I forgot one more 'do' to override the stronger binding of $: (n,) $ do reflect $ fld ast Great satisfaction! I killed all long-ranging parentheses! ;-) -- Andreas let headers = M.insert _report_ranges (format_two_tstamps rv) headers0 foldM write_period (rv,headers,(snd rv,snd rv)) asts return () where write_period (rv,headers,mv) ast = do pv@(p_valid_from,p_valid_until) - reflect $ get_trange TRange ast check_inside pv rv let prevailing = M.lookup PREVAILING ast (mv,pv) - case prevailing of Just _ - return (pv,pv)-- set the major valid period -- Make sure each VAR period occurs later than the prevailing -- period. If exactly at the same time add 1 min Nothing - case () of _ | fst mv p_valid_from - return (mv,pv) _ | fst mv == p_valid_from - return (mv,(p_valid_from + 60, p_valid_until)) _ - gthrow . InvalidData . unwords $ [ VAR period begins before prevailing:, show ast, ; prevailing TRange, show mv] let token = maybe (M.findWithDefault VAR ast) id prevailing let ast1 = M.insert _token token . M.insert _period_valid (format_two_tstamps pv) . M.unionWith (\_ x - x) headers $ ast let title = M.member Title ast let headers1 = if title then headers else M.delete _limit_to . M.delete _limit_recd $ headers write_fields h ast1 fields return (rv,headers1,mv) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Non-recursive let
Mmh, true, for polymorphic definitions there is not a lot to see. This probably diminishes the applicability of a strictness analysis quite a bit. Maybe it is entirely useless at this point. It would make more sense after whole-program optimization. Ghc does not have this, I heard the Intel Research Compiler does such things. This is becoming a very high-hanging fruit... --Andreas On 24.07.2013 20:22, Edward Kmett wrote: You only have a Num constraint when type checking that code: (+) :: Num a = a - a - a For better or worse, you don't get strictness in the type signatures in Haskell. We do not separate codata from data here. Without knowing about the particular instance of Num and even the direction of recursion on (+) there is no information for such a strictness analyzer to work with. many :: Alternative m = m a - m [a] many p = ps where ps = (:) $ p * ps | pure [] is another perfectly cromulent example of value recursion, and one that is far nearer and dearer to my heart and is similarly opaque to any such analysis. -Edward On Wed, Jul 24, 2013 at 4:14 AM, Andreas Abel andreas.a...@ifi.lmu.de mailto:andreas.a...@ifi.lmu.de wrote: Sure. I have not looked a concrete strictness analyses, but I expect they would treat Conat differently than Integer. In particular, x does *not* appear strictly in S x if S is a lazy constructor. On 22.07.13 4:54 PM, Edward Kmett wrote: let x = x +1 is perfectly cromulent when x is sufficiently lazy, e.g. in the one point compactification of the naturals: data Conat = S Conat | Z There it represents infinity with proper sharing. -Edward On Jul 22, 2013, at 10:24 AM, Andreas Abel andreas.a...@ifi.lmu.de mailto:andreas.a...@ifi.lmu.de wrote: On 22.07.2013 10:50, MigMit wrote: On Jul 22, 2013, at 12:27 PM, Andreas Abel andreas.a...@ifi.lmu.de mailto:andreas.a...@ifi.lmu.de wrote: On 20.07.13 9:36 PM, Evan Laforge wrote: However, I'm also not agitating for a non-recursive let, I think that ship has sailed. Besides, if it were added people would start wondering about non-recursive where, and it would introduce an exception to haskell's pretty consistently order-independent declaration style. For functions, recursive-by-default let makes sense. But for *values*, intended recursion is rather the exception. It is useful for infinite lists and the like. For values of atomic type like Int or Bool, recursive let is a bug. It seems hard to distinguish between them. What about values that contain functions, like data T = T Int (Int - Int)? What about polymorphic values, that could be functions and could be not? I agree. It cannot be implemented like that. A thing that could be implemented is that let x = e is an error if x appears strictly in e. In practice, this could catch some unintended cases of recursion like let x = x +1 , but not all of them. Cheers, Andreas -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de mailto:andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~__abel/ http://www2.tcs.ifi.lmu.de/~abel/ _ Haskell-Cafe mailing list Haskell-Cafe@haskell.org mailto:Haskell-Cafe@haskell.org http://www.haskell.org/__mailman/listinfo/haskell-cafe http://www.haskell.org/mailman/listinfo/haskell-cafe -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de mailto:andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~__abel/ http://www2.tcs.ifi.lmu.de/~abel/ -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Non-recursive let
On 25.07.2013 09:09, o...@okmij.org wrote: Here is a snippet from a real code that could benefit from non-recursive let. The example is notable because it incrementally constructs not one but two structures (both maps), ast and headers. The maps are constructed in a bit interleaved fashion, and stuffing them into the same State would be ungainly. In my real code -- Add an update record to a buffer file do_update :: String - Handle - Parsed - [Parsed] - IO () do_update TAF h ast asts@(_:_) = do rv - reflect $ get_trange TRange ast headers0 - return . M.fromList = sequence (map (\ (n,fld) - reflect (fld ast) = \v - return (n,v)) fields_header) This is a mouth-full. The = \v - return (n,v) can be more elegantly expressed with tuple section (map (\ (n,fld) - (n,) $ reflect (fld ast)) fields_header) Maybe even use mapSnd f = (id *** f) and write (map (mapSnd $ \ fld - reflect (fld ast)) fields_header) and, getting into lambda-killing rush :-) (map (mapSnd $ reflect . ($ ast)) fields_header) (ok, now we overdid it). Also, was not mapM = sequence . map ? And return . f = m the same as f $ m? Then we are at headers0 - M.fromList $ do mapM (\ (n,fld) - (n,) $ reflect (fld ast)) fields_header Actually, I prefer for-loops: headers0 - M.fromList $ do forM fields_header $ \ (n, fld) - do (n,) $ reflect $ fld ast Great satisfaction! I killed all long-ranging parentheses! ;-) -- Andreas let headers = M.insert _report_ranges (format_two_tstamps rv) headers0 foldM write_period (rv,headers,(snd rv,snd rv)) asts return () where write_period (rv,headers,mv) ast = do pv@(p_valid_from,p_valid_until) - reflect $ get_trange TRange ast check_inside pv rv let prevailing = M.lookup PREVAILING ast (mv,pv) - case prevailing of Just _ - return (pv,pv) -- set the major valid period -- Make sure each VAR period occurs later than the prevailing -- period. If exactly at the same time add 1 min Nothing - case () of _ | fst mv p_valid_from - return (mv,pv) _ | fst mv == p_valid_from - return (mv,(p_valid_from + 60, p_valid_until)) _ - gthrow . InvalidData . unwords $ [ VAR period begins before prevailing:, show ast, ; prevailing TRange, show mv] let token = maybe (M.findWithDefault VAR ast) id prevailing let ast1 = M.insert _token token . M.insert _period_valid (format_two_tstamps pv) . M.unionWith (\_ x - x) headers $ ast let title = M.member Title ast let headers1 = if title then headers else M.delete _limit_to . M.delete _limit_recd $ headers write_fields h ast1 fields return (rv,headers1,mv) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] memoization
Sorry I screwed up. The following is indeed memoizing: fib5 :: Int - Integer fib5 = \ x - fibs !! x where fibs = map fib [0 ..] fib 0 = 0 fib 1 = 1 fib n = fib5 (n-2) + fib5 (n-1) Here, the eta-expansion does not matter. But as you say, memoized_fib below is not memoizing, since x is in scope in the where clauses, even though they do not mention it. Thus, for each x we get new definitions of fibs and fib. Yet, this is only true for -O0. For -O1 and greater, ghc seems to see that x is not mentioned in the where clauses and apparently lifts them out. Thus, for -O1.. memoized_fib is also memoizing. (I ran it, this time ;-) !) Cheers, Andreas On 22.07.13 11:43 PM, Tom Ellis wrote: On Mon, Jul 22, 2013 at 04:16:19PM +0200, Andreas Abel wrote: In general, I would not trust such compiler magic, but just let-bind anything I want memoized myself: memoized_fib :: Int - Integer memoized_fib x = fibs !! x where fibs = map fib [0..] -- lazily computed infinite list fib 0 = 0 fib 1 = 1 fib n = memoized_fib (n-2) + memoized_fib (n-1) The eta-expansions do not matter. I meant to write Then, eta-expansions do not matter. (In general, they do matter.) But this is *not* memoized (run it and see!). The eta-expansions do indeed matter (although I don't think they are truly eta-expasions because of the desugaring of the where to a let). What matters is not the let binding, but where the let binding occurs in relation to the lambda. There's no compiler magic here, just operational semantics. Tom ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Non-recursive let
On 23.07.13 4:34 AM, Richard A. O'Keefe wrote: On 22/07/2013, at 8:14 PM, Andreas Abel wrote: Just today, my student asked me why the following program does nothing: Did you ask your student why their code should not be torn into pieces, burned to ashes, and incorporated into a pot for radioactive waste? All those occurrences of unsafePerformIO! No, here they are intended, to simulate something like uniqueness types in Clean, which incidentially has been mentioned on this thread before. The loop has nothing to do with unsafePerformIO, but stems from Haskell's idiosyncratic recursive let, which is a trap for all that come from another functional language. -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Non-recursive let
Sure. I have not looked a concrete strictness analyses, but I expect they would treat Conat differently than Integer. In particular, x does *not* appear strictly in S x if S is a lazy constructor. On 22.07.13 4:54 PM, Edward Kmett wrote: let x = x +1 is perfectly cromulent when x is sufficiently lazy, e.g. in the one point compactification of the naturals: data Conat = S Conat | Z There it represents infinity with proper sharing. -Edward On Jul 22, 2013, at 10:24 AM, Andreas Abel andreas.a...@ifi.lmu.de wrote: On 22.07.2013 10:50, MigMit wrote: On Jul 22, 2013, at 12:27 PM, Andreas Abel andreas.a...@ifi.lmu.de wrote: On 20.07.13 9:36 PM, Evan Laforge wrote: However, I'm also not agitating for a non-recursive let, I think that ship has sailed. Besides, if it were added people would start wondering about non-recursive where, and it would introduce an exception to haskell's pretty consistently order-independent declaration style. For functions, recursive-by-default let makes sense. But for *values*, intended recursion is rather the exception. It is useful for infinite lists and the like. For values of atomic type like Int or Bool, recursive let is a bug. It seems hard to distinguish between them. What about values that contain functions, like data T = T Int (Int - Int)? What about polymorphic values, that could be functions and could be not? I agree. It cannot be implemented like that. A thing that could be implemented is that let x = e is an error if x appears strictly in e. In practice, this could catch some unintended cases of recursion like let x = x +1 , but not all of them. Cheers, Andreas -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Non-recursive let
Just today, my student asked me why the following program does nothing:
{-# LANGUAGE CPP, GeneralizedNewtypeDeriving, BangPatterns #-}
import Control.Monad
import System.IO.Unsafe
import Data.Array.IO
import Data.IORef
import Debug.Trace
type LinearArray a = (Int, IORef Int, IOArray Int a)
initLinearArray :: Int - a - LinearArray a
initLinearArray l a =
trace init (
unsafePerformIO (do version - newIORef 0
array - newArray (0, l - 1) a
return (0, version, array)))
readLinearArray :: Int - (LinearArray a) - a
readLinearArray l !(ver, realver, arr) =
trace read (
unsafePerformIO (do version - readIORef realver
element - readArray arr l
if (version == ver) then
return element
else error Non-Linear read of linear Array))
writeLinearArray :: Int - a - LinearArray a - LinearArray a
writeLinearArray l e !(ver, realver, arr) =
trace write (
unsafePerformIO (do version - readIORef realver
if (version == ver)
then
do writeIORef realver $ ver + 1
writeArray arr l e
return (ver + 1, realver, arr)
else error Non-Linear write of linear Array))
linearArrayToList :: Int - Int - (LinearArray a) - [a]
linearArrayToList c m !a =
trace toList (
if (c = m) then []
else (readLinearArray c a) : (linearArrayToList (c + 1) m a))
eratostenesTest :: Int - [Bool]
eratostenesTest length =
let
strikeMult :: Int - Int - Int - (LinearArray Bool) -
(LinearArray Bool)
strikeMult div cur len arr = trace smStart (
if (cur = len)
then trace arr arr
else let arr = trace write $ writeLinearArray cur False arr
in trace strikeMult2 $ strikeMult div (cur + div) len arr)
nextPrime :: Int - Int - (LinearArray Bool) - (LinearArray Bool)
nextPrime cur len !arr =
if (cur = len)
then
arr
else if (readLinearArray cur arr)
then
let arr = trace strikeMult $ strikeMult cur (cur + cur)
len arr
in trace nextPrime $ nextPrime (cur + 1) len arr
else
nextPrime (cur + 1) len arr
ini = trace ini (initLinearArray length True)
theArray = trace nextPrimeCall $ nextPrime 2 length ini
in
linearArrayToList 0 length theArray
On 22.07.13 9:01 AM, Richard A. O'Keefe wrote:
On 21/07/2013, at 7:36 AM, Evan Laforge wrote:
Just by coincidence, I recently wrote this:
This is a BEAUTIFUL example.
I think we may disagree about what it's an example OF,
however. I found the code a little difficult to
follow, but when that's fixed up, there's no longer
any reason to want non-recursive let, OR a monad.
I've run out of time tonight, but hope to say more tomorrow.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Non-recursive let
On 20.07.13 9:36 PM, Evan Laforge wrote: However, I'm also not agitating for a non-recursive let, I think that ship has sailed. Besides, if it were added people would start wondering about non-recursive where, and it would introduce an exception to haskell's pretty consistently order-independent declaration style. For functions, recursive-by-default let makes sense. But for *values*, intended recursion is rather the exception. It is useful for infinite lists and the like. For values of atomic type like Int or Bool, recursive let is a bug. Of course, if you want to do scope-checking before type-checking, which also makes sense, you cannot make recursiveness type-dependent. Distinguishing 'let' into 'fun', 'val' and 'val rec' could help here: Non-recursive: val x = e in e' Recursive: fun f x = e in e' val rec x = e(x) in e' -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] memoization
On 22.07.2013 09:52, Chris Wong wrote: memoized_fib :: Int - Integer memoized_fib = (map fib [0 ..] !!) where fib 0 = 0 fib 1 = 1 fib n = memoized_fib (n-2) + memoized_fib (n-1) [.. snipped ..] Could someone explain the technical details of why this works? Why is map fib [0 ..] not recalculated every time I call memoized_fib? A binding is memoized if, ignoring everything after the equals sign, it looks like a constant. In other words, these are memoized: x = 2 Just x = blah (x, y) = blah f = \x - x + 1 -- f = ... and these are not: f x = x + 1 f (Just x, y) = x + y If you remove the right-hand side of memoized_fib, you get: memoized_fib = ... This looks like a constant. So the value (map fib [0..] !!) is memoized. If you change that line to memoized_fib x = map fib [0..] !! x GHC no longer memoizes it, and it runs much more slowly. True, but the essential thing to be memoized is not memoized_fib, which is a function, but the subexpression map fib [0..] which is an infinite list, i.e., a value. The rule must be like in let x = e if e is purely applicative, then its subexpressions are memoized. For instance, the following is also not memoizing: fib3 :: Int - Integer fib3 = \ x - map fib [0 ..] !! x where fib 0 = 0 fib 1 = 1 fib n = fib3 (n-2) + fib3 (n-1) In general, I would not trust such compiler magic, but just let-bind anything I want memoized myself: memoized_fib :: Int - Integer memoized_fib x = fibs !! x where fibs = map fib [0..] -- lazily computed infinite list fib 0 = 0 fib 1 = 1 fib n = memoized_fib (n-2) + memoized_fib (n-1) The eta-expansions do not matter. Cheers, Andreas -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Non-recursive let
On 22.07.2013 10:50, MigMit wrote: On Jul 22, 2013, at 12:27 PM, Andreas Abel andreas.a...@ifi.lmu.de wrote: On 20.07.13 9:36 PM, Evan Laforge wrote: However, I'm also not agitating for a non-recursive let, I think that ship has sailed. Besides, if it were added people would start wondering about non-recursive where, and it would introduce an exception to haskell's pretty consistently order-independent declaration style. For functions, recursive-by-default let makes sense. But for *values*, intended recursion is rather the exception. It is useful for infinite lists and the like. For values of atomic type like Int or Bool, recursive let is a bug. It seems hard to distinguish between them. What about values that contain functions, like data T = T Int (Int - Int)? What about polymorphic values, that could be functions and could be not? I agree. It cannot be implemented like that. A thing that could be implemented is that let x = e is an error if x appears strictly in e. In practice, this could catch some unintended cases of recursion like let x = x +1 , but not all of them. Cheers, Andreas -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Non-recursive let
On 17.07.13 9:46 PM, Edward Kmett wrote: FWIW, I maintain, according to wc and sloccount, 220841 lines worth of Haskell code at present. Thanks, this is great service to our community. And you produce excellent quality! I have been bitten this error one time, so it affects me .45% of the time and that was only because it was in the only package I was not using -Wall on. -Edward On Wed, Jul 17, 2013 at 12:23 PM, Andreas Abel andreas.a...@ifi.lmu.de mailto:andreas.a...@ifi.lmu.de wrote: Here, again, is your ACTUAL CODE, commented, deployed, looping, and maybe linked into your projects, if you are not careless about the cabal constraints: http://hackage.haskell.org/__packages/archive/mtl/2.1/doc/__html/src/Control-Monad-State-__Class.html#state http://hackage.haskell.org/packages/archive/mtl/2.1/doc/html/src/Control-Monad-State-Class.html#state -- | Embed a simple state action into the monad. state :: (s - (a, s)) - m a state f = do s - get let ~(a, s) = f s put s return a Have fun with it, Andreas On 17.07.2013 02:20, Richard A. O'Keefe wrote: Brian Marick sent me a couple of his stickers. The one I have on my door reads to be less wrong than yesterday. The other one I keep free to bring out and wave around: An example would be handy about now. All of the arguing to and fro -- including mine! -- about non-recursive let has been just so much hot air. I could go on about how the distinction between 'val' and 'val rec' in ML was one of the things I came to dislike intensely, and how Haskell's single coherent approach is one of the things that attracted me to Haskell. But why should anyone else care? When presented with a difficulty, it is very common for some functional language users to propose adding just one more feature from some other language, commonly an imperative one (which ML, Caml, and F# arguably are). Typically this is something that _would_ solve the immediate problem but would create worse problems elsewhere, and there is some other solution, either one already available in the language, or a better one that would solve additional problems or cause fewer ones. The best help for any discussion is A CONCRETE EXAMPLE OF REAL CODE. Not little sketches hacked up for the purpose of discussion, but ACTUAL CODE. The person who initially proposes a problem may think some details are not relevant, whereas someone else may see them as the key to the solution. For example, looking at some code in another mostly- functional language, which had been presented as reason why we needed a new construct, I rewrote it in less than half the number of lines using existing constructors, using only existing features. Without seeing THE ACTUAL CODE that prompted this thread, it is impossible to tell whether that might be the case here. In this specific case, we are seeing state being threaded through a bunch of updates, and IN THE ABSENCE OF THE ACTUAL CODE, it seems to me that monad notation is the most intention-revealing notation available for the purpose in Haskell, and if Haskell did have non-recursive let it would STILL be best to write such code using a state monad so that human beings reading the Haskell code would have some idea of what was happening, because that's how state changes are supposed to be expressed in Haskell, and anything else counts as obfuscation. But THE ACTUAL CODE might show that this case was different in some important way. _ Haskell-Cafe mailing list Haskell-Cafe@haskell.org mailto:Haskell-Cafe@haskell.org http://www.haskell.org/__mailman/listinfo/haskell-cafe http://www.haskell.org/mailman/listinfo/haskell-cafe -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de mailto:andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~__abel/ http://www2.tcs.ifi.lmu.de/~abel/ _ Haskell-Cafe mailing list Haskell-Cafe@haskell.org mailto:Haskell-Cafe@haskell.org http://www.haskell.org/__mailman/listinfo/haskell-cafe http://www.haskell.org/mailman/listinfo/haskell-cafe -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel
Re: [Haskell-cafe] Proposal: Non-recursive let
Here, again, is your ACTUAL CODE, commented, deployed, looping, and maybe linked into your projects, if you are not careless about the cabal constraints: http://hackage.haskell.org/packages/archive/mtl/2.1/doc/html/src/Control-Monad-State-Class.html#state -- | Embed a simple state action into the monad. state :: (s - (a, s)) - m a state f = do s - get let ~(a, s) = f s put s return a Have fun with it, Andreas On 17.07.2013 02:20, Richard A. O'Keefe wrote: Brian Marick sent me a couple of his stickers. The one I have on my door reads to be less wrong than yesterday. The other one I keep free to bring out and wave around: An example would be handy about now. All of the arguing to and fro -- including mine! -- about non-recursive let has been just so much hot air. I could go on about how the distinction between 'val' and 'val rec' in ML was one of the things I came to dislike intensely, and how Haskell's single coherent approach is one of the things that attracted me to Haskell. But why should anyone else care? When presented with a difficulty, it is very common for some functional language users to propose adding just one more feature from some other language, commonly an imperative one (which ML, Caml, and F# arguably are). Typically this is something that _would_ solve the immediate problem but would create worse problems elsewhere, and there is some other solution, either one already available in the language, or a better one that would solve additional problems or cause fewer ones. The best help for any discussion is A CONCRETE EXAMPLE OF REAL CODE. Not little sketches hacked up for the purpose of discussion, but ACTUAL CODE. The person who initially proposes a problem may think some details are not relevant, whereas someone else may see them as the key to the solution. For example, looking at some code in another mostly- functional language, which had been presented as reason why we needed a new construct, I rewrote it in less than half the number of lines using existing constructors, using only existing features. Without seeing THE ACTUAL CODE that prompted this thread, it is impossible to tell whether that might be the case here. In this specific case, we are seeing state being threaded through a bunch of updates, and IN THE ABSENCE OF THE ACTUAL CODE, it seems to me that monad notation is the most intention-revealing notation available for the purpose in Haskell, and if Haskell did have non-recursive let it would STILL be best to write such code using a state monad so that human beings reading the Haskell code would have some idea of what was happening, because that's how state changes are supposed to be expressed in Haskell, and anything else counts as obfuscation. But THE ACTUAL CODE might show that this case was different in some important way. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ordNub
On 14.07.2013 13:20, Niklas Hambüchen wrote:
I've taken the Ord-based O(n * log n) implementation from yi using a Set:
ordNub :: (Ord a) = [a] - [a]
ordNub l = go empty l
where
go _ [] = []
go s (x:xs) = if x `member` s then go s xs
else x : go (insert x s) xs
(The benchmark also shows some other potential problem: Using a state
monad to keep the set instead of a function argument can be up to 20
times slower. Should that happen?)
I cannot say whether this should happen, but your code about can be
straight-forwardly refactored using a *Reader* monad.
import Control.Monad.Reader
import Data.Functor (($))
import qualified Data.Set as Set
-- ifM still not in Control.Monad
ifM mc md me = do { c - mc; if c then md else me }
ordNub :: (Ord a) = [a] - [a]
ordNub l = runReader (go l) Set.empty
where
go [] = return []
go (x:xs) = ifM ((x `Set.member`) $ ask)
(go xs)
((x :) $ local (Set.insert x) (go xs))
test = ordNub [1,2,4,1,3,5,2,3,4,5,6,1]
Of course, this does not lend itself to an application of filterM.
In fact, your implementation is already in the (Set a -) reader monad,
in normalized form. It looks already optimal to me.
Cheers,
Andreas
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Non-recursive let
Ah, now I have the solution:
{-# LANGUAGE CPP #-}
(|) = flip ($)
#define LET(p, e) (e) | \ (p) -
bla = LET(x, 5)
LET(Just x, Just (x+1))
x
#define MLET(p, e) (e) | \ (p) - do
main = do
MLET((x, y), (5, 3))
print (x + y)
Beautiful, ain't it? Sigh.
--Andreas
On 11.07.2013 17:40, Carter Schonwald wrote:
Yup. Nested cases *are* non recursive lets.
(Can't believe I forgot about that )
On Thursday, July 11, 2013, Edward Kmett wrote:
blah = case foo 1 [] of
(x, s) - case bar x s of
(y, s) - case baz x y s of
(z, s) - ...
-Edward
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non-recursive let [Was: GHC bug? Let with guards loops]
On 12.07.2013 02:22, Richard A. O'Keefe wrote: For what it's worth, let x = 1 in - let x = x+1 in - let x = x+2 in - x;; prints val it : int = 4 in the F# interactive system, but let x = 1 in - let x = x+1 in - let x = x+2 in - x;; prints Duplicate definition of x at the second line. Since silverlight does not work properly on my systems, I cannot tryfsharp.org. I can try ocaml, which does not use indentation, and there the value is 4, and there is no ambiguity at all. let p = e in body is just (\ p - body) e it cannot be simpler than that. So I do not see your point. -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non-recursive let
Note that for non-recursive lets
let' x1 = e1
x2 = e2
is sequential and *not* the same as the parallel
let' (x1, x2) = (e1, e2)
The first is
(\ x1 - (\x2 - ...) e2) e1
and the second is
(\ (x1,x2) - ...) (e1, e2)
On 11.07.2013 13:36, Doug McIlroy wrote:
By analogy to ML, which has let and let rec, where the latter
corresponds to Haskell's let, one is led to let nonrec. I
would definitely not like shadow, for it means that new
variable does NOT cast a shadow on its definining expression.
I fear also that let nonrec by any name would introduce another
attractive nuisance, just as insidious as the one it is intended
to correct. For example
x = ...
let nonrec { x = someFunction x
xsq = x^2} in ...
won't do what was probably intended. In my own code, this idiom
is more likely than the one that sparked the discussion.
Doug
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Non-recursive let
I can do this without extra indentation:
(|) = flip ($)
f = 5 | \ x -
6 | \ y -
x + y
Non-recursive let is as superfluous as the do-notation.
On 11.07.2013 17:40, Carter Schonwald wrote:
Yup. Nested cases *are* non recursive lets.
(Can't believe I forgot about that )
On Thursday, July 11, 2013, Edward Kmett wrote:
On Wed, Jul 10, 2013 at 3:47 AM, o...@okmij.org javascript:_e({},
'cvml', 'o...@okmij.org'); wrote:
Jon Fairbairn wrote:
It just changes forgetting to use different variable names
because of
recursion (which is currently uniform throughout the language) to
forgetting to use non recursive let instead of let.
Let me bring to the record the message I just wrote on Haskell-cafe
http://www.haskell.org/pipermail/haskell-cafe/2013-July/109116.html
and repeat the example:
In OCaml, I can (and often do) write
let (x,s) = foo 1 [] in
let (y,s) = bar x s in
let (z,s) = baz x y s in ...
In Haskell I'll have to uniquely number the s's:
let (x,s1) = foo 1 [] in
let (y,s2) = bar x s1 in
let (z,s3) = baz x y s2 in ...
and re-number them if I insert a new statement.
blah = case foo 1 [] of
(x, s) - case bar x s of
(y, s) - case baz x y s of
(z, s) - ...
-Edward
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non-recursive let [Was: GHC bug? Let with guards loops]
Hi Oleg, just now I wrote a message to haskell-pr...@haskell.org to propose a non-recursive let. Unfortunately, the default let is recursive, so we only have names like let' for it. I also mentioned the ugly workaround (- return $) that I was shocked to see the first time, but use myself sometimes now. Cheers, Andreas On 10.07.2013 09:34, o...@okmij.org wrote: Andreas wrote: The greater evil is that Haskell does not have a non-recursive let. This is source of many non-termination bugs, including this one here. let should be non-recursive by default, and for recursion we could have the good old let rec. Hear, hear! In OCaml, I can (and often do) write let (x,s) = foo 1 [] in let (y,s) = bar x s in let (z,s) = baz x y s in ... In Haskell I'll have to uniquely number the s's: let (x,s1) = foo 1 [] in let (y,s2) = bar x s1 in let (z,s3) = baz x y s2 in ... and re-number them if I insert a new statement. BASIC comes to mind. I tried to lobby Simon Peyton-Jones for the non-recursive let a couple of years ago. He said, write a proposal. It's still being written... Perhaps you might want to write it now. In the meanwhile, there is a very ugly workaround: test = runIdentity $ do (x,s) - return $ foo 1 [] (y,s) - return $ bar x s (z,s) - return $ baz x y s return (z,s) After all, bind is non-recursive let. -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non-recursive let [Was: GHC bug? Let with guards loops]
On 10.07.2013 10:16, Ertugrul Söylemez wrote: o...@okmij.org wrote: Hear, hear! In OCaml, I can (and often do) write let (x,s) = foo 1 [] in let (y,s) = bar x s in let (z,s) = baz x y s in ... In Haskell I'll have to uniquely number the s's: let (x,s1) = foo 1 [] in let (y,s2) = bar x s1 in let (z,s3) = baz x y s2 in ... This isn't a case for non-recursive let. It is one of the rare cases where you might actually consider using a state monad. Except when you are implementing the state monad (giggle): http://hackage.haskell.org/packages/archive/mtl/2.1/doc/html/src/Control-Monad-State-Class.html#state -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non-recursive let [Was: GHC bug? Let with guardsloops]
Totality checking will generate a lot of false positives. One would like an analysis that prints an error message if an expression is *definitely* looping in all cases. While I have studied termination, I have not studied non-termination analyses. It is harder than termination. For termination checking, you can over-approximate the control-flows and just scream if you find a *potential* control flow that *might* lead to non-termination. If you do not find such a control flow you can be sure things are terminating. This is how Agda does it. To be sure that something is definitely non-terminating, you need to show it is non-terminating on all *actual* control flows. But usually you cannot statically tell whether in if c then d else e d or e is evaluated, so a non-termination analysis without false positives seems very restricted. Still it might be could useful. Having said this, having a termination analysis is not the proper solution to the lack of a non-recursive let, it does not establish shadowing behavior I want. Cheers, Andreas On 10.07.13 7:44 PM, Ertugrul Söylemez wrote: Donn Cave d...@avvanta.com wrote: Let is recursive because, unlike in the case of other languages, variables are not locations for storing values, but the expressions on the right side of the equality themselves. And obviously it is not possible for a variable-expression to be two expressions at the same time. The recursiveness is buildt-in. It comes from its pure nature. I'm surprised that it would come down to purity. It looks to me like simply a question of scope. I had to write an example program to see what actually happens, because with me it isn't intuitive at all that the name bound to an expression would be visible from within the expression itself. I suppose this is considered by some to be a feature, obviously to others it's a bug. In a non-strict-by-default language like Haskell it's certainly a feature. A sufficiently smart compiler can figure out whether a definition is recursive or not and apply the proper transformation, so from a language-theoretic standpoint there is really no reason to have a non-recursive let. I think the proper solution is to identify the underlying problem: general recursion. Haskell does not enforce totality. I'd really love to see some optional totality checking in Haskell. If Oleg decides not to use a state monad, he will still have to be careful not to confuse the numbers, but if he does, then the compiler will reject his code instead of producing looping code. Greets, Ertugrul -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Non-recursive let
On 10.07.13 9:31 PM, Carter Schonwald wrote:
theres a very simple way to do non recursive let already! do notation in
the identity monad. I use it quite a lot lately.
Yeah, the hack
x - return $ e
instead of
let x = e
has been discussed already.
If you put everything into the Identity monad, you lose if-then-else and
direct use of case, instead of
case me of {branches }
you need to write
e - me; case e of { branches }
This gets a bit better with the new \case, if you can afford to only
compile on the newest ghc.
me = \case { branches }
On Wed, Jul 10, 2013 at 1:49 PM, Ertugrul Söylemez e...@ertes.de
mailto:e...@ertes.de wrote:
Ezra e. k. Cooper e...@ezrakilty.net mailto:e...@ezrakilty.net
wrote:
As starter suggestions for the keyword or syntax, I submit:
let new x = expr in body -- Not the old x!
It's not the old x in either case (recursive and non-recursive).
let shadowing x = expr in body
shadow x = expr in body
It's shadowing in either case.
let x =! expr in body -- The explosive bang gives an imperative
flavor.
(=!) is a valid operator name.
Other suggestions would be welcome.
My suggestion: Don't add a non-recursive let. See my other post about
general recursion and totality checking.
Greets,
Ertugrul
--
Not to be or to be and (not to be or to be and (not to be or to be and
(not to be or to be and ... that is the list monad.
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non-recursive let [Was: GHC bug? Let with guardsloops]
On 10.07.13 6:00 PM, Donn Cave wrote: quoth Alberto G. Corona, Let is recursive because, unlike in the case of other languages, variables are not locations for storing values, but the expressions on the right side of the equality themselves. And obviously it is not possible for a variable-expression to be two expressions at the same time. The recursiveness is buildt-in. It comes from its pure nature. @Alberto: you must have misunderstood my proposal. I'm surprised that it would come down to purity. It looks to me like simply a question of scope. I had to write an example program to see what actually happens, because with me it isn't intuitive at all that the name bound to an expression would be visible from within the expression itself. I suppose this is considered by some to be a feature, obviously to others it's a bug. Value-recursion *is* useful in a lazy language, e.g. let xs = 0 : xs builds an infinite (in fact, circular) list of 0s. But it is not always meaningful, e.g. let x = x + 1 simply loops. I would like to be in the position to tell Haskell what I mean, whether I want recursion or not. I've gone to some trouble to dig up an nhc98 install (but can't seem to find one among my computers and GHC 7 won't build the source thanks to library re-orgs etc.) Because, I vaguely recall that nhc98's rules were different here? Anyone in a position to prove me wrong? I would doubt that nhc98 would interpret let xs = 0 : xs differently than ghc if it implemented anything close to the Haskell 98 standard. But I am not in a position to prove you wrong. Cheers, Andreas -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non-recursive let [Was: GHC bug? Let with guards loops]
On 10.07.13 11:42 AM, Ertugrul Söylemez wrote: I think we are all aware that shadowing is a bad idea, no matter whether you do it through Identity or non-recursive let. WHAT?? [This is Richard Bird's WHAT?? when someone said that using folds is like programming in assembly language.] How can you think this if we say we WANT shadowing?! Also if you are serious about this, you would have to make non-recursive let the default to get OCaml-style behavior, which would be an extremely invasive change. We would have to fix pretty much all packages, all tutorials, all books, all wiki pages, etc. Otherwise just like you may forget to renumber your variables, you may just as well forget to add the norec keyword or whatever the syntax would be. Wow, this is getting really dramatic now. Don't be afraid, now one will force you to shadow any of your identifiers... -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] GHC bug? Let with guards loops
Hi, is this a known bug or feature of GHC (7.4.1, 7.6.3)?:
I got a looping behavior in one of my programs and could not explain
why. When I rewrote an irrefutable let with guards to use a case
instead, the loop disappeared. Cut-down:
works = case Just 1 of { Just x | x 0 - x }
loops = let Just x | x 0 = Just 1 in x
works returns 1, loops loops. If x is unused on the rhs, the
non-termination disappears.
works' = let Just x | x 0 = Just 1 in 42
Is this intended by the Haskell semantics or is this a bug? I would
have assumed that non-recursive let and single-branch case are
interchangeable, but apparently, not...
Cheers,
Andreas
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GHC bug? Let with guards loops
Thanks, Dan and Roman, for the explanation. So I have to delete the
explanation non-recursive let = single-branch case from my brain.
I thought the guards in a let are assertations, but in fact it is more
like an if. Ok.
But then I do not see why the pattern variables are in scope in the
guards in
let p | g = e
The variables in p are only bound to their values (given by e) if the
guard g evaluates to True. But how can g evaluate if it has yet unbound
variables? How can ever a pattern variable of p be *needed* to compute
the value of the guard? My conjecture is that it cannot, so it does not
make sense to consider variables of g bound by p. Maybe you can cook up
some counterexample.
I think the pattern variables of p should not be in scope in g, and
shadowing free variables of g by pattern variables of p should be forbidden.
Cheers,
Andreas
On 09.07.2013 17:05, Dan Doel wrote: The definition
Just x | x 0 = Just 1
is recursive. It conditionally defines Just x as Just 1 when x 0 (and
as bottom otherwise). So it must know the result before it can test the
guard, but it cannot know the result until the guard is tested. Consider
an augmented definition:
Just x | x 0 = Just 1
| x = 0 = Just 0
What is x?
On 09.07.2013 17:49, Roman Cheplyaka wrote:
As Dan said, this behaviour is correct.
The confusing thing here is that in case expressions guards are attached
to the patterns (i.e. to the lhs), while in let expressions they are
attached to the rhs.
So, despite the common Just x | x 0 part, your examples mean rather
different things.
Here's the translation of 'loops' according to the Report:
loops =
let Just x =
case () of
() | x 0 - Just 1
in x
Here it's obvious that 'x' is used in the rhs of its own definition.
Roman
* Andreas Abel andreas.a...@ifi.lmu.de [2013-07-09 16:42:00+0200]
Hi, is this a known bug or feature of GHC (7.4.1, 7.6.3)?:
I got a looping behavior in one of my programs and could not explain
why. When I rewrote an irrefutable let with guards to use a case
instead, the loop disappeared. Cut-down:
works = case Just 1 of { Just x | x 0 - x }
loops = let Just x | x 0 = Just 1 in x
works returns 1, loops loops. If x is unused on the rhs, the
non-termination disappears.
works' = let Just x | x 0 = Just 1 in 42
Is this intended by the Haskell semantics or is this a bug? I would
have assumed that non-recursive let and single-branch case are
interchangeable, but apparently, not...
Cheers,
Andreas
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GHC bug? Let with guards loops
Hi Felipe, thanks for the centavos.
So you mean that in
let p | g = e where bs
in ...
the bindings bs should be in scope in g (and of course the variables of
p are in scope in bs). Mmh, the bindings in bs that do not uses the
pattern variables could be useful in g, but the other bindings will
still lead to non-termination. Maybe such an analysis is too
sophisticated. My lesson is to use case instead of let. Only that the
let syntax is nicer and indentation-friendlier than case, so it would be
preferable.
The greater evil is that Haskell does not have a non-recursive let.
This is source of many non-termination bugs, including this one here.
let should be non-recursive by default, and for recursion we could have
the good old let rec.
Cheers,
Andreas
On 09.07.2013 19:23, Felipe Almeida Lessa wrote:
Well, you could use p's type for something.
let x | foo (undefined `asTypeOf` x) = 3
foo _ = True
in x
Arguably not very useful. It seems to me that the most compelling
rationale is being consistent with the cases where, instead of being a
data type, p is a function. Even so most of the time you won't be
recursing on the guard. But, since you could use something from the
where clause on the guard, and we certainly won't be restricting
recursing on the where clause, it also seems compelling to allow
recursion on the guard.
My 2 centavos, =)
On Tue, Jul 9, 2013 at 2:12 PM, Andreas Abel andreas.a...@ifi.lmu.de wrote:
Thanks, Dan and Roman, for the explanation. So I have to delete the
explanation non-recursive let = single-branch case from my brain.
I thought the guards in a let are assertations, but in fact it is more like
an if. Ok.
But then I do not see why the pattern variables are in scope in the guards
in
let p | g = e
The variables in p are only bound to their values (given by e) if the guard
g evaluates to True. But how can g evaluate if it has yet unbound
variables? How can ever a pattern variable of p be *needed* to compute the
value of the guard? My conjecture is that it cannot, so it does not make
sense to consider variables of g bound by p. Maybe you can cook up some
counterexample.
I think the pattern variables of p should not be in scope in g, and
shadowing free variables of g by pattern variables of p should be forbidden.
Cheers,
Andreas
On 09.07.2013 17:05, Dan Doel wrote: The definition
Just x | x 0 = Just 1
is recursive. It conditionally defines Just x as Just 1 when x 0 (and
as bottom otherwise). So it must know the result before it can test the
guard, but it cannot know the result until the guard is tested. Consider
an augmented definition:
Just x | x 0 = Just 1
| x = 0 = Just 0
What is x?
On 09.07.2013 17:49, Roman Cheplyaka wrote:
As Dan said, this behaviour is correct.
The confusing thing here is that in case expressions guards are attached
to the patterns (i.e. to the lhs), while in let expressions they are
attached to the rhs.
So, despite the common Just x | x 0 part, your examples mean rather
different things.
Here's the translation of 'loops' according to the Report:
loops =
let Just x =
case () of
() | x 0 - Just 1
in x
Here it's obvious that 'x' is used in the rhs of its own definition.
Roman
* Andreas Abel andreas.a...@ifi.lmu.de [2013-07-09 16:42:00+0200]
Hi, is this a known bug or feature of GHC (7.4.1, 7.6.3)?:
I got a looping behavior in one of my programs and could not explain
why. When I rewrote an irrefutable let with guards to use a case
instead, the loop disappeared. Cut-down:
works = case Just 1 of { Just x | x 0 - x }
loops = let Just x | x 0 = Just 1 in x
works returns 1, loops loops. If x is unused on the rhs, the
non-termination disappears.
works' = let Just x | x 0 = Just 1 in 42
Is this intended by the Haskell semantics or is this a bug? I would
have assumed that non-recursive let and single-branch case are
interchangeable, but apparently, not...
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GHC bug? Let with guards loops
On 09.07.2013 19:56, Dan Doel wrote:
With pattern guards, it's difficult to say whether it is never 'useful'
to have things like the following work:
C x | C' y z - f x = ...
But I'd also shy away from changing the behavior because it causes a lot
of consistency issues. In
let
f vs1 | gs1 = es1
h vs2 | gs2 = es2
...
we have that f and h are in scope in both gs1 and gs2. Does it make
sense to call f in gs1? It's easy to loop if you do. So should f not be
in scope in gs1, but h is, and vice versa for gs2? But they're both in
scope for es1 and es2?
If f and h are really mutually recursive, then they should not be in
scope in gs1 and gs2.
If the first thing you do in the body of f is calling f (which happens
if f appears in gs1), then you are bound to loop. But of course, if vs
are not just variables but patterns, then the first thing you do is
matching, so using f in gs1 could be fine.
I am getting on muddy grounds here, better retreat. I was thinking only
of non-recursive let.
In the report
http://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-440003.12
it says that
let p = e1 in e0= case e1 of ~p - e0
where no variable in p appears free in e1
but this applies only for patterns p without guards, and I would have
expected to be true also for patterns with guards.
And if we leave the above alone, then what about the case where there
are no vs? Is that different? Or is it only left-hand patterns that
get this treatment?
Yes, it is only about the things defined by the let binding (in this
case, f and g). The variables in vs1 are bound by calling f, but by f's
body.
Also, it might have some weird consequences for moving code around. Like:
let Just x | x 0 = Just 1
Non-recursive.
let Just x | y 0 = Just 1
y = x
Recursive.
let Just x | b = Just 1
where b = x 0
Recursive?
let Just x | b = Just 1
b = x 0
Recursive. (Like 2.)
These all behave the same way now. Which ones should change?
Only the first one? Hard to tell.
If Haskell had a non-recursive let, that'd probably be a different
story. But it doesn't.
Definitely agree.
On Tue, Jul 9, 2013 at 1:12 PM, Andreas Abel andreas.a...@ifi.lmu.de
mailto:andreas.a...@ifi.lmu.de wrote:
Thanks, Dan and Roman, for the explanation. So I have to delete the
explanation non-recursive let = single-branch case from my brain.
I thought the guards in a let are assertations, but in fact it is
more like an if. Ok.
But then I do not see why the pattern variables are in scope in the
guards in
let p | g = e
The variables in p are only bound to their values (given by e) if
the guard g evaluates to True. But how can g evaluate if it has yet
unbound variables? How can ever a pattern variable of p be *needed*
to compute the value of the guard? My conjecture is that it cannot,
so it does not make sense to consider variables of g bound by p.
Maybe you can cook up some counterexample.
I think the pattern variables of p should not be in scope in g, and
shadowing free variables of g by pattern variables of p should be
forbidden.
Cheers,
Andreas
On 09.07.2013 17:05, Dan Doel wrote: The definition
Just x | x 0 = Just 1
is recursive. It conditionally defines Just x as Just 1 when x
0 (and
as bottom otherwise). So it must know the result before it can
test the
guard, but it cannot know the result until the guard is tested.
Consider
an augmented definition:
Just x | x 0 = Just 1
| x = 0 = Just 0
What is x?
On 09.07.2013 17:49, Roman Cheplyaka wrote:
As Dan said, this behaviour is correct.
The confusing thing here is that in case expressions guards are
attached
to the patterns (i.e. to the lhs), while in let expressions they are
attached to the rhs.
So, despite the common Just x | x 0 part, your examples mean
rather
different things.
Here's the translation of 'loops' according to the Report:
loops =
let Just x =
case () of
() | x 0 - Just 1
in x
Here it's obvious that 'x' is used in the rhs of its own definition.
Roman
* Andreas Abel andreas.a...@ifi.lmu.de
mailto:andreas.a...@ifi.lmu.de [2013-07-09 16:42:00+0200]
Hi, is this a known bug or feature of GHC (7.4.1, 7.6.3)?:
I got a looping behavior in one of my programs and could not
explain
why. When I rewrote an irrefutable let with guards to use a
case
instead, the loop disappeared. Cut-down:
works = case Just 1 of { Just x | x 0 - x }
loops = let Just x | x 0
Re: [Haskell-cafe] mapFst and mapSnd
See Agda.Utils.Tuple :-) -- | Bifunctoriality for pairs. (-*-) :: (a - c) - (b - d) - (a,b) - (c,d) (f -*- g) ~(x,y) = (f x, g y) -- | @mapFst f = f -*- id@ mapFst :: (a - c) - (a,b) - (c,b) mapFst f ~(x,y) = (f x, y) -- | @mapSnd g = id -*- g@ mapSnd :: (b - d) - (a,b) - (a,d) mapSnd g ~(x,y) = (x, g y) I think mapPair, mapFst, and mapSnd are canonical names that could be added to Data.Tuple. But if you suggest this on librar...@haskell.org, you get probably turned down, see e.g. http://comments.gmane.org/gmane.comp.lang.haskell.libraries/17411 Cheers, Andreas On 28.05.2013 15:34, Petr Pudlák wrote: Dne 28.5.2013 10:54, Dominique Devriese napsal(a): Hi all, I often find myself needing the following definitions: mapPair :: (a - b) - (c - d) - (a,c) - (b,d) mapPair f g (x,y) = (f x, g y) mapFst :: (a - b) - (a,c) - (b,c) mapFst f = mapPair f id mapSnd :: (b - c) - (a,b) - (a,c) mapSnd = mapPair id But they seem missing from the prelude and Hoogle or Hayoo only turn up versions of them in packages like scion or fgl. Has anyone else felt the need for these functions? Am I missing some generalisation of them perhaps? Apart from Arrows, there is also package bifunctors that defines this functionality for (,), Either and a few others: http://hackage.haskell.org/packages/archive/bifunctors/3.2.0.1/doc/html/Data-Bifunctor.html Petr Pudlak ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Lambda Calculus question on equivalence
The answer to your question is given in Boehm's theorem, and the answer is no, as you suspect. For the untyped lambda-calculus, alpha-equivalence of beta-eta normal forms is the same as observational equivalence. Or put the other way round, two normal forms which are not alpha-equivalent can be separated by an observation L. Cheers, Andreas On 03.05.2013 00:33, Roman Cheplyaka wrote: IIRC, Barendregt'84 monography (The Lambda Calculus: Its Syntax and Semantics) has a significant part of it devoted to this question. * Ian Price ianpric...@googlemail.com [2013-05-02 20:47:07+0100] Hi, I know this isn't perhaps the best forum for this, but maybe you can give me some pointers. Earlier today I was thinking about De Bruijn Indices, and they have the property that two lambda terms that are alpha-equivalent, are expressed in the same way, and I got to wondering if it was possible to find a useful notion of function equality, such that it would be equivalent to structural equality (aside from just defining it this way), though obviously we cannot do this in general. So the question I came up with was: Can two normalised (i.e. no subterm can be beta or eta reduced) lambda terms be observationally equivalent, but not alpha equivalent? By observationally equivalent, I mean A and B are observationally equivalent if for all lambda terms L: (L A) is equivalent to (L B) and (A L) is equivalent to (B L). The definition is admittedly circular, but I hope it conveys enough to understand what I'm after. My intuition is no, but I am not sure how to prove it, and it seems to me this sort of question has likely been answered before. Cheers -- Ian Price -- shift-reset.com Programming is like pinball. The reward for doing it well is the opportunity to do it again - from The Wizardy Compiled ___ 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 -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Conflicting bindings legal?!
Hi Tillmann,
no, I am not against shadowing. It's a two-edged sword, but I find it
very useful.
Shadowing is very intuitive if one can proceed in a left-to-right,
top-to-bottom order, just as one reads. Then it is clear that the later
occurrence of a binding shadows the earlier one. No formal spec. is
needed to resolve binding in that case.
The confusion comes when one binding comes from a 'where' which is below
the use, and another comes from a 'do' or 'let' which is above the use.
Then there is no trivial intuitive reading (especially if the block
structure is implicit and handled by indentation).
Cheers,
Andreas
On 26.02.2013 10:57, Tillmann Rendel wrote:
Hi,
Andreas Abel wrote:
To your amusement, I found the following in the Agda source:
abstractToConcreteCtx :: ToConcrete a c = Precedence - a - TCM c
abstractToConcreteCtx ctx x = do
scope - getScope
let scope' = scope { scopePrecedence = ctx }
return $ abstractToConcrete (makeEnv scope') x
where
scope = (currentScope defaultEnv) { scopePrecedence = ctx }
I am surprised this is a legal form of shadowing. To understand which
definition of 'scope' shadows the other, I have to consult the formal
definition of Haskell.
Isn't this just an instance of the following, more general rule:
To understand what a piece of code means, I have to consult the formal
definition of the language the code is written in.
In the case you cite, you just have to desugar the do notation
abstractToConcreteCtx :: ToConcrete a c = Precedence - a - TCM c
abstractToConcreteCtx ctx x =
getScope = (\scope -
let scope' = scope { scopePrecedence = ctx } in
return $ abstractToConcrete (makeEnv scope') x)
where
scope = (currentScope defaultEnv) { scopePrecedence = ctx }
and it becomes clear by the nesting structure that the lambda-binding
shadows the where-binding. It seems that if you argue against this case,
you argue against shadowing in general. Should we adopt the Barendregt
convention as a style guide for programming?
Tillmann
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Conflicting bindings legal?!
To your amusement, I found the following in the Agda source:
abstractToConcreteCtx :: ToConcrete a c = Precedence - a - TCM c
abstractToConcreteCtx ctx x = do
scope - getScope
let scope' = scope { scopePrecedence = ctx }
return $ abstractToConcrete (makeEnv scope') x
where
scope = (currentScope defaultEnv) { scopePrecedence = ctx }
I am surprised this is a legal form of shadowing. To understand which
definition of 'scope' shadows the other, I have to consult the formal
definition of Haskell.
But I studied computer science to *not* become a lawyer!!
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Conflicting bindings legal?!
Luckily, {-# OPTIONS -fwarn-unused-binds #-} saves me from searching for
the formal spec...
On 26.02.13 10:25 AM, Andreas Abel wrote:
To your amusement, I found the following in the Agda source:
abstractToConcreteCtx :: ToConcrete a c = Precedence - a - TCM c
abstractToConcreteCtx ctx x = do
scope - getScope
let scope' = scope { scopePrecedence = ctx }
return $ abstractToConcrete (makeEnv scope') x
where
scope = (currentScope defaultEnv) { scopePrecedence = ctx }
I am surprised this is a legal form of shadowing. To understand which
definition of 'scope' shadows the other, I have to consult the formal
definition of Haskell.
But I studied computer science to *not* become a lawyer!!
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] mtl: Why there is Monoid w constraint in the definition of class MonadWriter?
return = MyWriter 0 MyWriter n x = k = let MyWriter n' y = k x in MyWriter (n+n') y instance MonadWriter Integer MyWriter where tell n = MyWriter n () listen (MyWriter n x) = return (x,n) pass (MyWriter n (a,f)) = MyWriter (f n) a Yes, integers do form a monoid when equipped with 0 and (+). However, we know well why they are not an instance of Monoid — namely, there's more than one way they form a monoid. Even if something is in theory a monoid, there may be technical reasons not to declare it a Monoid. Likewise, imposing a (technical) superclass constraint on MonadWriter has nothing to do with whether the Monad will be well-behaved. This is true in both directions: even if the type is an instance of Monoid, nothing forces the Monad instance to use the Monoid instance. I.e. I can declare a MonadWriter on the Sum newtype whose bind, instead of adding, subtracts the numbers. Roman -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lambda case
Right, case..of is superfluous,
case e of
branches
can now be written as
e | \case
branches
with backwards application | (or some prefer --- sadly, the proposal
to add backwards appliation to base did not make it to a consensus).
This is in accordance to the monadic
me = \case
branches
If there was an opportunity to make drastic language changes, case..of
could be disposed of altogether. \case could become 'cases' or 'match'
or 'fun' (rather not 'of', for my taste).
The current compromise it not too bad, I think.
Unfortunately, I have to wait for 7.6 to become the standard before
using \case in Agda source...
Cheers,
Andreas
On 30.11.12 7:25 AM, Herbert Valerio Riedel wrote:
Jon Fairbairn jon.fairba...@cl.cam.ac.uk writes:
[...]
“\case” complicates lambda, using “of” simply breaks “case … of …”
into two easily understood parts.
Just some observation (I'm rather late to the lambda-case discussion, so
this might have been already pointed out previously):
if the reserved keyword 'of' was to take the place of '\case', shouldn't
then
'case' exp
w/o the 'of' { alts }-part become a separately valid expression (with
'case' essentially meaning 'flip ($)') to really break it up into two
independent parts? Then 'case exp of { alts }' wouldn't be a special
form anymore, but would just result from combining 'case' and 'of';
'case' wouldn't even need to be a reserved keyword (and thus the grammar
could be simplified), if it wasn't for the current grammar which
requires to isolate a \case-expression by using () or $, consider e.g.:
{-# LANGUAGE LambdaCase #-}
import System.Environment
case' :: b - (b - c) - c
case' = flip ($)
main = do
s - getArgs
case' s $ \case -- image '\case' was actually '\of' or 'of'
[x] - putStrLn (Hello ++ x)
_ - putStrLn wrong number of arguments given
just my 2¢
cheers,
hvr
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is anyone working on a sparse matrix library in Haskell?
Hi Mark, I might become your user. Currently, for Agda I have rolled my own sparse matrix implementation, see http://hackage.haskell.org/packages/archive/Agda/latest/doc/html/src/Agda-Termination-SparseMatrix.html Cheers, Andreas On 29.11.12 5:03 PM, Mark Flamer wrote: I am looking to continue to learn Haskell while working on something that might eventually be useful to others and get posted on Hackage. I have written quite a bit of Haskell code now, some useful and a lot just throw away for learning. In the past others have expressed interest in having a native Haskell sparse matrix and linear algebra library available(not just bindings to a C lib). This in combination with FEM is one of my interests. So my questions, is anyone currently working on a project like this? Does it seem like a good project/addition to the community? I'm also interested if anyone has any other project idea's, maybe even to collaborate on. Thanks -- View this message in context: http://haskell.1045720.n5.nabble.com/Is-anyone-working-on-a-sparse-matrix-library-in-Haskell-tp5721452.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lambda case (was Re: A big hurray for lambda-case (and all the other good stuff))
I had been missing a pattern matching lambda in Haskell for a long time
(SML had fn since ages) and my typical use will be
monadic_expr = \case
branches
I think \case is not the worst choice, certainly better than of ...
Thanks to the GHC 7.6 developers!
Cheers,
Andreas
On 29.11.12 12:49 PM, Jon Fairbairn wrote:
Ben Franksen ben.frank...@online.de writes:
just wanted to drop by to say how much I like the new lambda case extension.
I use it all the time and I just *love* how it relieves me from conjuring up
dummy variables, which makes teh code not only esier to write but also to
read.
[…] should *definitely* go into Haskell'13.
As I was opposed to the suggestion for lambda case I didn’t
really follow the discussion of the syntax, but I’m puzzled by
the choice. To me it seems obvious that if we are going to do
this (as opposed to something more decomposable like
lambda-match), we should do it simply by making the “case exp”
part of a case expression optional. So the syntax for lambda-
case would be
of {alts…}
and we would then describe
case e of {…}
as syntactic sugar for
(of {…}) (e)
Doing it this way doesn’t introduce any new syntactic elements
and has fewer tokens at the point of use.
I don’t see any need for a \ in the syntax: this is a functional
language we are talking about after all. Once we know that “of”
introduces a function, that should be enough.
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Taking over ghc-core
Excellent! With ghc-core being maintained again, we can start thinking about compiling Agda to core instead of hs. Andreas On 11.11.12 11:41 AM, Bas van Dijk wrote: Great! On 10 November 2012 16:17, Shachaf Ben-Kiki shac...@gmail.com wrote: With Don Stewart's blessing (https://twitter.com/donsbot/status/267060717843279872), I'll be taking over maintainership of ghc-core, which hasn't been updated since 2010. I'll release a version with support for GHC 7.6 later today. Shachaf ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] mtl-2.1 severly broken, cabal needs blacklisting
After 2 days of shrinking 251 modules of source code to a few lines I realized that modify in MonadState causes loop in mtl-2.1. http://hackage.haskell.org/packages/archive/mtl/2.1/doc/html/src/Control-Monad-State-Class.html#modify The bug has been fixed, apparently seven month ago. https://github.com/ekmett/mtl/pull/1 However, the malicious mtl-2.1 still lingers on: it is available from hackage and installed in many systems. This calls for a means of blacklisting broken or malicious packages. cabal update should also pull a blacklist of packages that will never be selected by cabal install (except maybe by explicit user safety overriding). I think such a mechanism is not only necessary for security purposes, but also to safe the valuable resources of our community. Cheers, Andreas -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] mtl-2.1 severly broken, cabal needs blacklisting
On 13.11.2012 17:39, Dan Burton wrote: Mixed feelings here. I personally subscribe to the philosophy of do one thing and do it well; perhaps this sort of functionality would be better delegated to a new curation tool such as the one described in Michael Snoyman's recent blog post. http://www.yesodweb.com/blog/2012/11/solving-cabal-hell I think Michael Snoyman's approach goes farther than mine and solves a slightly different problem. I am not concerned with the dependency hell but with a means of safely avoiding bugged packages. Uploading a bugged package can happen to anyone of us, but cabal/hackage does not provide a suitable means to rectify the situation. Cabal's philosophy currently includes a monotonicity assumption: newer is better and more correct. As a consequence, packages do not get removed or replaced since that could break compilation of other packages depending on a special version number of a package. The calamity is that bugged package live on, and cabal install is oblivious of this. If one could blacklist a certain version of a package, cabal could pick the next higher available version, as a sort of redirection mechanism to the fixed package. For instance, if I have issued mylib-2.1 mylib-2.2 mylib-3.0 and I discover a bug in mylib-2.1, I could blacklist mylib-2.1 and upload a bugfix version mylib-2.1.1 that would be picked by cabal instead of mylib-2.1. Those user packages that rely on the specific interface of mylib-2.1 (e.g. having a constraint mylib == 2.1) and do not work with mylib-2.2 would still work, since they would be built with mylib-2.1.1 On Tue, Nov 13, 2012 at 9:27 AM, Andreas Abel andreas.a...@ifi.lmu.de mailto:andreas.a...@ifi.lmu.de wrote: After 2 days of shrinking 251 modules of source code to a few lines I realized that modify in MonadState causes loop in mtl-2.1. http://hackage.haskell.org/__packages/archive/mtl/2.1/doc/__html/src/Control-Monad-State-__Class.html#modify http://hackage.haskell.org/packages/archive/mtl/2.1/doc/html/src/Control-Monad-State-Class.html#modify The bug has been fixed, apparently seven month ago. https://github.com/ekmett/mtl/__pull/1 https://github.com/ekmett/mtl/pull/1 However, the malicious mtl-2.1 still lingers on: it is available from hackage and installed in many systems. This calls for a means of blacklisting broken or malicious packages. cabal update should also pull a blacklist of packages that will never be selected by cabal install (except maybe by explicit user safety overriding). I think such a mechanism is not only necessary for security purposes, but also to safe the valuable resources of our community. Cheers, Andreas -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] hackageDB haddock errors
I found that for the recently uploaded Agda-2.3.2 there is no haddockumentation. Stumbling over the build protocol by chance http://hackage.haskell.org/packages/archive/Agda/2.3.2/logs/success/ghc-7.6 I searched for whether haddock had been executed and found, yes, but also, it failed: ... 40% ( 2 / 5) in 'Agda.Syntax.Abstract.Pretty' haddock: internal error: /tmp/ghc17357_0/ghc17357_126.s: hPutBuf: resource exhausted (No space left on device) Q: Could this build be run again, with sufficient disk space? For gtk-0.12.4 there is another explanation: it has build failures: http://hackage.haskell.org/packages/archive/gtk/0.12.4/logs/failure/ghc-7.6 On 13.11.2012 16:41, timothyho...@seznam.cz wrote: Hello, There are several packages without haddock documentation on hackage. The one that bugs me right now, is the latest version of gtk2hs: http://hackage.haskell.org/package/gtk I've been told that this may be due to hackage updating docs with an infrequent cron job, so that new packages don't get their docs for a long time. Whatever is causing it, the fact that hayoo http://holumbus.fh-wedel.de/hayoo/hayoo.html always uses the most frequent docs, means that I cannot currently search for anything gtk2hs related :( Can someone please look into prodding this cron job so it doesn't take days to run, or look into resolving any errors that might be causing this unfortunate behaviour? Thank you for your time, and happy hacking, Timothy -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] mtl-2.1 severly broken, cabal needs blacklisting
On 13.11.12 11:13 PM, Jean-Philippe Bernardy wrote: Blacklisting equals releasing a bugfix. Not quite. Using version number conventions, identifying such a release should be easy. If there exists a bugfix release for a package currently in use, then cabal should emit a warning. Warnings are easily overlooked. In a typical cabal install session I see tons of irrelevant warnings floating by. On Nov 13, 2012 6:12 PM, Andreas Abel andreas.a...@ifi.lmu.de mailto:andreas.a...@ifi.lmu.de wrote: On 13.11.2012 17:39, Dan Burton wrote: Mixed feelings here. I personally subscribe to the philosophy of do one thing and do it well; perhaps this sort of functionality would be better delegated to a new curation tool such as the one described in Michael Snoyman's recent blog post. http://www.yesodweb.com/blog/__2012/11/solving-cabal-hell http://www.yesodweb.com/blog/2012/11/solving-cabal-hell I think Michael Snoyman's approach goes farther than mine and solves a slightly different problem. I am not concerned with the dependency hell but with a means of safely avoiding bugged packages. Uploading a bugged package can happen to anyone of us, but cabal/hackage does not provide a suitable means to rectify the situation. Cabal's philosophy currently includes a monotonicity assumption: newer is better and more correct. As a consequence, packages do not get removed or replaced since that could break compilation of other packages depending on a special version number of a package. The calamity is that bugged package live on, and cabal install is oblivious of this. If one could blacklist a certain version of a package, cabal could pick the next higher available version, as a sort of redirection mechanism to the fixed package. For instance, if I have issued mylib-2.1 mylib-2.2 mylib-3.0 and I discover a bug in mylib-2.1, I could blacklist mylib-2.1 and upload a bugfix version mylib-2.1.1 that would be picked by cabal instead of mylib-2.1. Those user packages that rely on the specific interface of mylib-2.1 (e.g. having a constraint mylib == 2.1) and do not work with mylib-2.2 would still work, since they would be built with mylib-2.1.1 On Tue, Nov 13, 2012 at 9:27 AM, Andreas Abel andreas.a...@ifi.lmu.de mailto:andreas.a...@ifi.lmu.de mailto:andreas.a...@ifi.lmu.__de mailto:andreas.a...@ifi.lmu.de wrote: After 2 days of shrinking 251 modules of source code to a few lines I realized that modify in MonadState causes loop in mtl-2.1. http://hackage.haskell.org/packages/archive/mtl/2.1/doc/html/src/Control-Monad-State-Class.html#modify http://hackage.haskell.org/__packages/archive/mtl/2.1/doc/__html/src/Control-Monad-State-__Class.html#modify http://hackage.haskell.org/__packages/archive/mtl/2.1/doc/__html/src/Control-Monad-State-__Class.html#modify http://hackage.haskell.org/packages/archive/mtl/2.1/doc/html/src/Control-Monad-State-Class.html#modify The bug has been fixed, apparently seven month ago. https://github.com/ekmett/mtl/pull/1 https://github.com/ekmett/mtl/__pull/1 https://github.com/ekmett/__mtl/pull/1 https://github.com/ekmett/mtl/pull/1 However, the malicious mtl-2.1 still lingers on: it is available from hackage and installed in many systems. This calls for a means of blacklisting broken or malicious packages. cabal update should also pull a blacklist of packages that will never be selected by cabal install (except maybe by explicit user safety overriding). I think such a mechanism is not only necessary for security purposes, but also to safe the valuable resources of our community. Cheers, Andreas -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de mailto:andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~__abel/ http://www2.tcs.ifi.lmu.de/~abel/ _ Libraries mailing list librar...@haskell.org mailto:librar...@haskell.org http://www.haskell.org/__mailman/listinfo/libraries http://www.haskell.org/mailman/listinfo/libraries -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman
Re: [Haskell-cafe] more sharing in generated code
On 03.11.12 10:05 AM, Peter Divianszky wrote:
Suppose we have a record update
r { x = f (r x)}
and suppose that most of the time f returns it's argument unchanged.
Recently I've heard about Q-combinators.
Central idea: Change (f :: a - a) to (f' :: a - Maybe a) returning
Nothing when the value didn't change.
Then we can replace the record update with smarter code which
preserves more sharing.
Just adding a remark here: I actually played with these Q-combinators,
they actually worsened performance of Agda. The problem is that they
make the code strict. The performance loss due to strictness
outweighted the potential performance gain by increased sharing.
Q-combinators were developed by John Harrison in the context of ML,
which is strict anyway.
I guess a compiler support for smart record update would not have the
strictness penalty.
Cheers,
Andreas
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Agda] How to avoid T3 fonts in pdf generated with lhs2TeX?
Hi,
I found the problem, it solved itself with an update of the TeXLive suite...
https://github.com/kosmikus/lhs2tex/issues/24
Thanks for your help!
Andreas
On 01.11.12 11:15 PM, Dominique Devriese wrote:
Andreas,
2012/11/1 Andreas Abel andreas.a...@ifi.lmu.de:
Hello,
maybe someone has experience in publishing papers that use lhs2TeX and
unicode characters with ACM, and has been in my situation before...
Sheridan, who publishes for ACM, does not like T3 fonts. However, lhs2tex
--agda does make use of T3 fonts via:
\RequirePackage[utf8x]{inputenc}
If I remove this, my unicode characters are garbled in the lhs2tex-generated
code. Does anoyone know a smart workaround besides replacing all the unicode
characters manually by some math symbols in the .tex file?
Not sure about all this, but perhaps you can try to use utf8 instead
of utf8x and manually define translations for the unicode characters
that you use,e.g.:
\DeclareUnicodeCharacter{2032}{'}
\DeclareUnicodeCharacter{2080}{_0}
\DeclareUnicodeCharacter{2081}{_1}
\DeclareUnicodeCharacter{2082}{_2}
\DeclareUnicodeCharacter{2115}{\mathbb{N}}
\DeclareUnicodeCharacter{2192}{\to}
\DeclareUnicodeCharacter{2200}{\forall\,}
Perhaps you can then somehow avoid translations that use T3 fonts (not
sure what these are though). Note: the numbers are the characters'
unicode hexadecimal representation (AFAIU), which you can find e.g.
using emacs's describe-char.
Dominique
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] How to avoid T3 fonts in pdf generated with lhs2TeX?
Hello,
maybe someone has experience in publishing papers that use lhs2TeX and
unicode characters with ACM, and has been in my situation before...
Sheridan, who publishes for ACM, does not like T3 fonts. However,
lhs2tex --agda does make use of T3 fonts via:
\RequirePackage[utf8x]{inputenc}
If I remove this, my unicode characters are garbled in the
lhs2tex-generated code. Does anoyone know a smart workaround besides
replacing all the unicode characters manually by some math symbols in
the .tex file?
Cheers,
Andreas
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why Kleisli composition is not in the Monad signature?
When I teach my students Haskell's monads, I never put Kleisli into my mouth. I tell them that monads are for sequencing effects; and the sequencing is visible clearly in () :: IO a - IO b - IO b (=) :: IO a - (a - IO b) - IO b but not in fmap :: (a - b) - IO a - IO b join :: IO (IO a) - IO a To me, print 1 print 2 looks natural, and print 1 = const (print 2) still understandable, but join $ fmap (const (print 2)) (print 1) rather not (I needed ghci to get this example right). I would not want to introduce category theory or Kleisli composition just to teach my students some effectful Haskell programming. Cheers, Andreas On 16.10.2012 21:45, Simon Thompson wrote: Not sure I really have anything substantial to contribute, but it's certainly true that if you see a - m b as a generalisation of the usual function type, a - b, then return generalises the identity and kleisli generalises function composition. This makes the types pretty memorable (and often the definitions too). Simon On 16 Oct 2012, at 20:14, David Thomas davidleotho...@gmail.com wrote: class Monad m where return :: a - m a kleisli :: (a - m b) - (b - m c) - (a - m c) Simon Thompson | Professor of Logic and Computation School of Computing | University of Kent | Canterbury, CT2 7NF, UK s.j.thomp...@kent.ac.uk | M +44 7986 085754 | W www.cs.kent.ac.uk/~sjt ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Over general types are too easy to make.
list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Andreas AbelDu bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.a...@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell's type inference considered harmful
Thanks for your answer and your examples. It would be worthwile
collecting such examples in a small article.
I think some of the problems with type inference come from insufficient
theory about metavariables. When I started studying higher-order
unification I always wondered what the scope of a metavariable is. It
is created at some point and then just sits there waiting to be solved
by a constraint. However, it is not clear where these constraints may
come from and at what time a metavariable should be declared unsolved or
be generalized over.
In the HM toy calculus (lambda + let), it is spelled out:
generalization must happen after a let, such that the solution for a
metavariable is determined solely by constraints in the *definition* of
a symbol, not in its *use*.
I'd be grateful for pointers to work that considers metavariable scope
in some bigger, more realistic calculi. In Haskell, one thing that goes
wrong is that all definitions in a module are considered mutually
recursive by the type inference algorithm. But in fact, the definitions
can be stratified by a strongly connected components analysis. Doing
such an analysis, and limiting metavariable scope to an SCC, would
overcome the problem I outlined in my original mail and would result in
a more principled treatment of metavariables.
That concerned type inference for global definitions. It is not clear
we want the same for local definitions. There, it makes more sense to
assume that the programmer can overlook what he is doing, and thus one
could allow flow of information from the use of a symbol to its
definition.
Do we want information flow from dead code to live code? I'd say no.
Dead is unfortunately undecidable; but at least one can identify
unused local definitions, i.e., statically unreachable definitions.
Your examples seem to suggest you want such information flow, or maybe not?
On 21.07.2012 12:26, o...@okmij.org wrote:
However, if your are using ExtendedDefaultRules then you are likely to
know you are leaving the clean sound world of type inference.
First of all, ExtendedDefaultRules is enabled by default in
GHCi. Second, my example will work without ExtendedDefaultRules, in
pure Haskell98. It is even shorter:
instance Num Char
main = do
x - return []
let y = x
print . fst $ (x, abs $ head x)
-- let dead = if False then y == else True
return ()
The printed result is either [] or .
Mainly, if the point is to demonstrate the non-compositionality of type
inference and the effect of the dead code, one can give many many
examples, in Haskell98 or even in SML.
Here is a short one (which does not relies on defaulting. It uses
ExistentialQuantification, which I think is in the new standard or is
about to be.).
{-# LANGUAGE ExistentialQuantification #-}
data Foo = forall a. Show a = Foo [a]
main = do
x - return []
let z = Foo x
let dead = if False then x == else True
return ()
The code type checks. If you _remove_ the dead code, it won't. As you
can see, the dead can have profound, and beneficial influence on
alive, constraining them. (I guess this example is well-timed for Obon).
Ah, I have never been in Japan at that time.
For another example, take type classes. Haskell98 prohibits overlapping of
instances. Checking for overlapping requires the global analysis of the
whole program and is clearly non-compositional. Whether you may define
instance Num (Int,Int)
depends on whether somebody else, in a library you use indirectly,
has already introduced that instance. Perhaps that library is imported
for a function that has nothing to do with treating a pair of Ints as
a Num -- that is, the instance is a dead code for your
program. Nevertheless, instances are always imported, implicitly.
Yes, that's a known problem.
The non-compositionality of type inference occurs even in SML (or
other language with value restriction). For example,
let x = ref [];;
(* let z = if false then x := [1] else ();; *)
x := [true];;
This code type checks. If we uncomment the dead definition, it
won't. So, the type of x cannot be fully determined from its
definition; we need to know the context of its use -- which is
precisely what seems to upset you about Haskell.
To stirr action, mails on haskell-cafe seem useless.
What made you think that? Your questions weren't well answered? What
other venue would you propose?
Yes, they were. But for discussion about metavariables maybe something
like a haskell implementor's forum would be more appropriate. Yet I am
only an Agda implementor.
Cheers,
Andreas
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe
Re: [Haskell-cafe] Haskell's type inference considered harmful
Haha, I like this example.
However, if your are using ExtendedDefaultRules then you are likely to
know you are leaving the clean sound world of type inference. The
example of my student works on plain GHC...
The other responses to my message confined to point me to best
practices to avoid the design bugs of Haskell's type inference.
However, if I want best practices, I can go to JavaScript.
To stirr action, mails on haskell-cafe seem useless.
I am already biased towards Haskell. But as an unbiased decision maker,
I would not consider a language with undead code for my projects...
Cheers,
Andreas
On 17.07.12 10:46 AM, o...@okmij.org wrote:
1. Haskell's type inference is NON-COMPOSITIONAL!
Yes, it is -- and there are many examples of it. Here is an example
which has nothing to do with MonomorphismRestriction or numeric
literals
{-# LANGUAGE #-}
class C a where
m :: a - Int
instance C () where
m _ = 1
instance C Bool where
m _ = 2
main = do
x - return undefined
let y = x
print . fst $ (m x, show x)
-- let dead = if False then not y else True
return ()
The program prints 1. If you uncomment the (really) dead code, it will
print 2. Why? The dead code doesn't even mention x, and it appears
after the printing! What is the role of show x, which doesn't do anything?
Exercises: what is the significance of the monadic bind to x? Why
can't we replace it with let x = undefined?
[Significant hint, don't look at it]
Such a behavior always occurs when we have HM polymorphism restriction
and some sort of non-parametricity -- coupled with default rules or
overlapping instances or some other ways of resolving overloading. All
these features are essential (type-classes are significant,
defaulting is part of the standard and is being used more and more).
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Haskell's type inference considered harmful [Re: [Haskell] A riddle...]
[Is Haskell-Cafe the right place to discuss DESIGN issues of the Haskell
language? This message is not about a concrete problem...]
Congratulations to all that solved the riddle so quickly. (First answer
in only 8 Minutes!) Now to the point of the exercise: Shocking
realizations.
1. Haskell's type inference is NON-COMPOSITIONAL!
In the riddle below, I am defining two things f (rgbliste) and g
(farbliste). Even though they are not strongly connected, but g comes
after f in the definition order, the code of g influences the type of f.
THAT'S WRONG! :-(
It gets worse:
2. DEAD CODE changes a program's result!
Yes indeed. Dead code (farbliste) in the source cannot be removed
safely. And:
3. Haskell casts 181935629 to Word16 value 7693 WITHOUT WARNING!
Needless to say, these are serious problems for leading-edge strongly
typed language. The experts are probably aware of this. But I awoke
harshly from a sweet dream.
Issue 3 is quite harmful and reminds me more of C than of a strongly
typed language. Fixing this is not trivial. The problem is that all
numeric constants have type Num a = a, and of course, type variable a
can be instantiated to Int Word16 or whatever. Numeric constants need
to inhabit subclasses of Num, e.g., Word16, Int and Integer /classes/ to
make this behavior go away.
Update: There is nothing wrong with Word16 computing modulo 2^16, but a
literal like 181935629 should not get type Word16 without warning. Java
asks for explicit casts in
byte i = (byte) 1234876;
but mindlessly also in
byte i = (byte) 123;
which is not a great solution either.
Issues 1/2 go away with
{-# LANGUAGE NoMonomorphismRestriction #-}
(thx to Christian who pointed me to this). I wonder why this is not on
by default?! There seems to be an unresolved dispute about this...
http://hackage.haskell.org/trac/haskell-prime/wiki/NoMonomorphismRestriction
But even with MonomorphismRestriction, issue 1/2 are avoidable with a
more refined approach to type meta variables in the Haskell type
inference: After type-checking a strongly connected component, type
meta variables created for this part of the Haskell program should not
be instantiated in the (topologically) later defined parts of the
program. YOU DON'T WANT THE USE OF A FUNCTION INFLUENCE ITS DEFINITION!
There are two alternatives what to do with remaining meta-variables of
a SCC:
1. With monomorphism restriction: instantiate to the best type.
In our example below, Haskell chooses Integer.
2. Without monomorphism restriction: generalize.
Choice 1 will give an error in the program below, but i rather have an
error than a silent change of behavior of my program!
Cheers,
Andreas
P.S.: In Agda, in the situation of unsolved metas in an SCC (a mutual
block), these metas are just frozen, triggering typing errors later
(since Agda cannot generalize). The user has to go back an insert more
type annotations. But this is safe, whereas silent late instantiation
breaks compositionality.
On 16.07.2012 17:25, Andreas Abel wrote:
Today a student came to me with a piece of code that worked it executed
by itself, but produced different result in the context of his larger
problem. We cut down the example to the following:
import Graphics.UI.Gtk
-- should produce [(26471,0,65535),...
rgbliste =
(map (\ i -
let rb = 5 * (mod (mod 181935629 (4534+i)) 100)-250+128 in
let gb = 5 * (mod (mod 128872693 (5148+i)) 100)-250+128 in
let bb = 5 * (mod (mod 140302469 (7578+i)) 100)-250+128 in
let r = min 255 $ max 0 rb in
let g = min 255 $ max 0 gb in
let b = min 255 $ max 0 bb in
(r*257,g*257,b*257)) [0..])
--farbliste = map (\ (r,g,b) - Color r g b) rgbliste
main :: IO ()
main = do
print $ head rgbliste
If you run it, it prints (26471,0,65535).
If you uncomment the def. of farbliste, it prints (44461,65535,65535).
I was surprised. What is going on?
Cheers,
Andreas
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
