November 2010 - Haskell-Cafe

Re: Making monadic code more concise
by oleg＠okmij.org 17 Nov '10

17 Nov '10

Ling Yang wrote > I think a good question as a starting point is whether it's possible > to do this 'monadic instance transformation' for any typeclass, and > whether or not we were lucky to have been able to instance Num so > easily (as Num, Fractional can just be seen as algebras over some base > type plus a coercion function, making them unusually easy to lift if > most typeclasses actually don't fit this description). > > In general, what this seems to be is a transformation on functions > that also depends explicitly on type signatures. For example in Num: Things start to break down when we get to the higher order. In the first order, it is indeed easy to see that the monadification of the term Int -> Int -> Int should/could be m Int -> m Int -> m Int Indeed, liftM2 realizes this transformation. But what about (Int -> Int) -> Int ? Should it be (m Int -> m Int) -> m Int ? A moment of thought shows that there is no total function of the type Monad m => ((Int -> Int) -> Int) -> ((m Int -> m Int) -> m Int) because there is no way, in general, to get from (m Int -> m Int) to the pure function Int->Int. That is, we can't write Monad m => (m Int -> m Int) -> m (Int->Int) One may try tabulation (for finite domains) tf f = do vt <- f (return True) vf <- f (return False) return $ \x -> if x then vt else vf but that doesn't quite work: what if the resulting function is never invoked on the True argument. We have needlessly computed that value, vt. Worse, we have incurred the effect of computing vt; that effect could be failure. We have needlessly failed. One can say: we need runnable > class (Monad m) => Runnable m where > exit : m a -> a are there many monads that are members of that typeclass? For example, Maybe cannot be Runnable; otherwise, what is (exit Nothing)? Any Error or MonadPlus monad can't be Runnable.

3 4

Re: ANNOUNCE zeno 0.1.0
by Petr Pudlak 16 Nov '10

16 Nov '10

Hi Will, I was wondering, Zeno capable of proving just equational statements, or is it able to prove more general statements about programs? In particular, it would be interesting if Zeno would be able to prove that a function is total by verifying that it uses only structural (inductive) recursion (on a well defined inductive type), i.e. each recursive function call must be on a syntactic subcomponent of its parameter. And dually, one might want to prove that a function is corecursive, meaning that each recursive call is guarded by a constructor. Best regards, Petr > Hi all, > > My masters project Zeno was recently mentioned on this mailing list so > I thought I'd announce that I've just finished a major update to it, > bringing it slightly closer to being something useful. Zeno is a fully > automated inductive theorem proving tool for Haskell programs. You can > express a property such as "takeWhile p xs ++ dropWhile p xs === xs" > and it will prove it to be true for all values of p :: a -> Bool and > xs :: [a], over all types a, using only the function definitions. > > Now that it's updated it can use polymorphic types/functions, and you > express properties in Haskell itself (thanks to SPJ for the > suggestion). It still can't use all of Haskell's syntax: you can't > have internal functions (let/where can only assign values), and you > can't use type-classed polymorphic variables in function definitions - > you'll have to create a monomorphic instance of the function -but I > hope to have these added reasonably soon. It's also still missing > primitive-types/IO/imports so it still can't be used with any > real-world Haskell code, it's more a bit of theorem proving "fun". > > You can try it out at http://www.doc.ic.ac.uk/~ws506/tryzeno, the code > file given there has some provable properties about a few prelude > functions among other things. > > Another feature is that it lists all the sub-properties it has proven > within each proof. When it verifies insertion-sort "sorted (insertsort > xs) === True" it also proves the antisymmetry of "<=" and that the > "insert" function preserves the "sorted" property. > > Any suggestions or feedback would be greatly appreciated. > > Cheers, > > Will

5 7

typeclass namespace rational?
by Jonathan Geddes 16 Nov '10

16 Nov '10

cafe, Data Constructors and Type Constructors don't share the same namespace. You see code like the following all the time: > data MyRecord = MyRecord {...} This is possible because Data Constructors are used in different parts of the code than Type Constructors so there's never any ambiguity. Type Classes, on the other hand, share the same namespace as Type Constructors. You can't define this: >class String s where > ... > >instance String String where > ... >instance String ByteString where > ... >instance String Text where > ... Not that I'm running out of valid haskell identifiers or anything :P, I'm just wondering: what's the rationale behind keeping Type Classes and Type Constructors in the same namespace? I can't think of any ambiguity there would be if they each had their own namespace. And In some cases it would be convenient to be able to define both a concrete representation and an abstract one with the same name as in the String class example above. --Jonathan

3 3

Re: [Haskell] intent-typing
by Tillmann Rendel 16 Nov '10

16 Nov '10

Hi, Marcus Sundman wrote: > Hi, how would one go about implementing (or using if it's supported > out-of-the-box) intent-typing* for haskell? A basic technique is to use newtype declarations to declare separate types for separate intents. module StringSafety ( SafeString () , UnsafeString () , quote , considerUnsafe ) where newtype SafeString = SafeString String newtype UnsafeString = UnsafeString String considerUnsafe :: String -> UnsafeString considerUnsafe s = UnsafeString s quote :: UnsafeString -> SafeString quote (UnsafeString s) = SafeString s' where s' = ... s ... This module does not export the SafeString and UnsafeString constructors, so we can be sure that no other code in the program can invent SafeStrings which are not really safe. Every string can be safely treated as unsafe, however, so we export a function considerUnsafe which does so. Now, if we type our interface to the outside world as getInput :: ... -> UnsafeString sendOutput :: SafeString -> ... we can be sure that a return value from getInput needs to pass through quote on its way to sendOutput, because quote is the only way to produce a SafeString. This guarantuees safety. It has, however, a practical problem: We can't use the usual String functions on UnsafeString or SafeString values. For instance, we can't concatenate two UnsafeStrings using (++). A naive solution would be to provide separate (++) functions for unsafe and safe strings: append_safe :: SafeString -> SafeString -> SafeString append_safe (SafeString x) (SafeString y) = SafeString (x ++ y) append_unsafe :: SafeString -> SafeString -> SafeString append_unsafe (UnsafeString x) (UnsafeString y) = UnsafeString (x ++ y) Note that at least append_safe needs to be implemented in and exported from the StringSafety module. That is a good thing, because this function needs to be carefully checked for safety. The programmer needs to prove (or unit-test, or at least think about) the following theorem: If a and b are safe strings, so is a ++ b. After this fact has been established, other modules are free to use append_safe however they like without possibly compromising safety. Now, the above approach should work, but is still rather impractical: We need to copy the definitions of all String functions for unsafe and safe strings. However, since the bodies of all these copies are actually identical, so we can use parametric polymorphism to abstract over the difference between UnsafeString and SafeString. One way to achieve this is to use phantom types. With phantom types, we declare only a single newtype for both safe and unsafe strings, but we annotate that type with an additional flag to distinguish safe from unsafe uses. module StringSafety ( AnnotatedString () , Safe () , Unsafe () , quote , considerUnsafe , append ) where data Safe = Safe data Unsafe = Unsafe newtype AnnotatedString safety = AnnotatedString String considerUnsafe :: String -> AnnotatedString Unsafe considerUnsafe s = AnnotatedString s quote :: AnnotatedString Unsafe -> AnnotatedString Safe quote (AnnotatedString s) = AnnotatedString s' where s' = ... s ... append :: AnnotatedString a -> AnnotatedString a -> AnnotatedString a append (AnnotatedString x) (AnnotatedString y) = AnnotatedString (x ++ y) Note that AnnotatedString does not really use its type parameter safety: That's why it is called a phantom type. The data constructor AnnotatedString can be freely used to convert between safe and unsafe strings, so we better not export it from the module. Inside the module, uses of the data constructor gives rise to proof obligations as above. So the programmer needs to reason that the following is true to justify the implementation and export of append: If x and y have the same safety level, then (x ++ y) has again that same safety level. So now, we still have to write a wrapper around each string operation, but at least we need to write only one such wrapper for all intents, not a separate wrapper for each intent. There is an inconvenience left: We can't concatenate safe and unsafe strings, because both arguments to append need to have exactly the same type. To fix this, we first have to figure out what the result of sucha concatenation would be: It would be an unsafe string, because at least one of the inputs is unsafe. We need to teach this kind of reasoning to the compiler, for instance, using type families: type family Join a b type instance Join Safe Safe = Safe type instance Join Safe Unsafe = Unsafe type instance Join Unsafe Safe = Unsafe type instance Join Unsafe Unsafe = Unsafe The idea is that (Join a b) is the safety level of the result of an operation which consumes data of safety level a and b. I called the type family Join because the safety levels form a lattice, with unsafe levels higher then safe levels, and the type family computes the join operation for that lattice. So we are encoding a simple static analysis into the type system here! Using this lattice structure of safety level, we can give a more polymorphic type to append: append :: AnnotatedString a -> AnnotatedString b -> AnnotatedString (Join a b) The implementation can remain unchanged. Now, the programmer needs to reason that the following statement is true to justify this type of append: (x ++ y) is at least as safe as the least safe of x and y. So to conclude, statically checked intent-typing can be expressed in Haskell using newtype wrappers with phantom types, and possibly some type-level computation on these phantom types to teach the compiler domain knowledge about the intents. Tillmann PS. Crossposted to the haskell cafe, please consider dropping haskell(a)haskell.org when answering.

3 2

Re: Add haskell-src as an official machine-readable component of the Haskell standard
by Niklas Broberg 16 Nov '10

16 Nov '10

(Moving to Café) > (Examples of controversies possible in haskell-src: we have the Hs > prefix on constructors everywhere, we can't provide fixity information > (and the haskell-src-exts implementation of this is unsatisfactory in > several important ways) ... What ways? http://trac.haskell.org/haskell-src-exts/ :-) Cheers, /Niklas

2 1

Bracket around every IO computation monad
by Mitar 16 Nov '10

16 Nov '10

Hi! I have a class Neuron which has (among others) two functions: attach and deattach. I would like to make a way to call a list/stack/bunch of attach functions in a way that if any of those fail (by exception), deattach for previously already attached values (called attach on them) are deattached (called deattach on them). I have come up with such way: data Growable where Growable :: Neuron n => LiveNeuron n -> Growable growNeurons :: [IO Growable] -> IO [Growable] growNeurons attaches = growNeurons' attaches [] where growNeurons' [] ls = return ls growNeurons' (a:ats) ls = bracketOnError a (\(Growable l) -> deattach l) (\l -> growNeurons' ats (l:ls)) So I give growNeurons a list of attach actions and it returns a list of attached values ((live)neurons). This works nice, but syntax to use it is ugly: neurons <- growNeurons [ do { a <- attach nerve1; return $ Growable a }, do { a <- attach nerve2; return $ Growable a }, do { a <- attach nerve3; return $ Growable a } ] Types of attach and deattach are (if I simplify): attach :: Nerve n -> IO (LiveNeuron n) deattach :: LiveNeuron n -> IO () Growable is only used so that I can put actions of different type in the list. It seems to me that all this could be wrapped into a monad. So that I would be able to call something like: neurons <- growNeurons' $ do attach nerve1 attach nerve2 attach nerve3 Where I would be allowed to call actions of a special type class which defined also clean-up function (in my case called deattach). And which would be called if there was any exception thrown (and then at the end rethrown). Otherwise, the result would be a list of all computed values. In my case all this in IO monad. So it is possible that evaluation of monad actions would be stacked inside of bracketOnError and in a case of error clean-up functions would be called, otherwise returns a list of results? Mitar

5 14

Updating Haskell Packages through Archlinux becoming A Pain
by Mathew de Detrich 16 Nov '10

16 Nov '10

Well basically, I haven't update my Haskell libraries for some time now (around a month) so when I finally got around to updating my Haskell packages (which are installed through Archlinux's AUR) my GHC installation broke (again). This has been happening for some time now (I have been having this problem for around a year) Basically it occurs when pacman updates a package using an AUR package, which cabal refuses to install because it can break other packages (yet the package still gets installed according to pacman). So this means I have to manually go through /usr/lib/ghc-6.12.3/package.conf.d and manually updating all the package hashes while doing some manual dependency tracking through ghc-check This honestly starting to become annoying, is there any ideas or plans on how to resolve this issue. The end user shouldn't have to be dealing with this, and if installing a package can break the system, it shouldn't be 'semi' installed in the first place

4 5

Annual dutch functional programming day, january 7 2011
by Christiaan Baaij 16 Nov '10

16 Nov '10

The annual Dutch functional programming day will take place soon: Date: Friday, January 7th, 2011 Location: University of Twente, Enschede During the day there will be several presentation related to FP-oriented research results, the use of FP concepts in industry, and the use of FP in education. Of course there is also plenty of opportunity to talk, exchange information, give demo's, and to meet old friends. Most participants are 'advanced' functional programmers; but those who recently developed an interest in all that is FP are of course more than welcome to join. Tradition dictates that at the end of the day we will enjoy a dinner together with those who wish join (at your own costs). You can register for the event by sending an email to me, Christiaan Baaij (c.p.r.baaij(a)utwente.nl) More information can be found at the website: http://caes.ewi.utwente.nl/External/NLFP Please indicate if you want to give presentation, and if you like to attend the dinner afterwards. Please also register if you only want to participate, as we have to know for how many people we should order lunch. There is of course NO participation fee. See you the 7th of January! Christiaan Baaij

1 0

dynamic loading of code on windows
by Arnaud Bailly 16 Nov '10

16 Nov '10

Hello, I recently tried to cabal install plugins on a windows box and it failed with the following error: Resolving dependencies... Downloading plugins-1.5.1.4... Configuring plugins-1.5.1.4... cabal: The package has a './configure' script. This requires a Unix compatibility toolchain such as MinGW+MSYS or Cygwin. cabal: Error: some packages failed to install: plugins-1.5.1.4 failed during the configure step. The exception was: ExitFailure 1 What solution can I use to load dynamically code in a cross-platform way ? Thanks in advance Arnaud

5 8

Quasiquoter invocation no longer requires/allows a leading dollar sign.
by Michael Snoyman 16 Nov '10

16 Nov '10

Sorry, maybe I missed the memo on this one, but I just noticed this change to quasi-quotation syntax on the GHC 7 upgrade page[1]. So if GHC 6.12 *requires* the dollar sign, and GHC 7 *rejects* the dollar sign, is there any way to write code that will run on both? Is there a reason we can't keep the dollar sign as supported syntax for a release or two to make for a cleaner migration? Michael [1] http://haskell.org/haskellwiki/Upgrading_packages/Updating_to_GHC_7#Quasiqu…

3 4