- Haskell-Cafe - Haskell.org

Re: coherence when overlapping?
by oleg＠pobox.com 17 Apr '06

17 Apr '06

> But I am still confused by the exact definition of coherence in the case of > overlapping. Does the standard coherence theorem apply? If yes, how? > If no, is there a theorem? Yes, the is, by Martin Sulzmann et al, the Theory of overloading (the journal version) http://www.comp.nus.edu.sg/~sulzmann/ms_bib.html#overloading-journal A simple intuition is this: instance selection may produce more than one candidate instance. Having inferred a polymorphic type with constraints, the compiler checks to see of some of the constraints can be reduced. If an instance selection produces no candidate instances, the typechecking failure is reported. If there is exactly one candidate instance, it is selected and the constraint is removed because it is resolved. An instance selection may produce more then one candidate instance. Those candidate instances may be incomparable: for example, given the constraint "C a" and instances "C Int" and "C Bool", both instances are candidates. If such is the case, the resolution of that constraint is deferred and it `floats out', to be incorporated into the type of the parent expression, etc. In the presence of overlapping instances, the multiple candidate instances may be comparable, e.g. "C a" and "C Int". The compiler then checks to see if the target type is at least as specific as the most specific of those candidate instances. If so, the constraint is reduced; otherwise, it is deferred. Eventually enough type information is available to reduce all constraints (or else it is a type error).

3 4

Re: [Haskell] ANNOUNCE: An index-aware linear algebra library in Haskell
by Alberto Ruiz 16 Apr '06

16 Apr '06

On Friday 14 April 2006 17:02, Frederik Eaton wrote: > An index-aware linear algebra library in Haskell Excellent work! Is it possible to create a vector or matrix whose size is not known at compile time? > - Due to the need to specify index types at some point, input of > vectors is difficult. I have provided two functions in Fu.Vector.Base > which should cover most of the cases: > > listVec :: Vector v e => [e] -> (forall n . (ReflectNum n) => v (L n) -> w) > -> w > listMat :: Vector v e => [[e]] -> > (forall n m . (ReflectNum n, ReflectNum m) => v (L m, L n) -> w) -> w > > However, these aren't useful in interactive situations. So I have also > provided some template-haskell routines > > http://ofb.net/~frederik/futility/src/Vector/Template.hs > > which can be used to instantiate vectors directly. For example: (In examples.hs): >-- matrix with elements of type Double >v6 = trans $(dAM [[1,2,3,4]]) > >v7 = $(dAM [[1,0,0],[0,1,0],[0,0,1],[1,1,1]]) -- Alberto

2 3

Re: [Haskell-cafe] Code Review: Sudoku solver
by Michael Hanus 16 Apr '06

16 Apr '06

Jared Updike wrote: > On 3/22/06, David F. Place <d(a)vidplace.com> wrote: > ... > > It solves > > sudoku puzzles. (What pleasure do people get by doing these in their > > heads?!?) > > > > They are probably asking the same question: why take hours to write a > program to do it when with my mad sudoku solving skills I can solve it > in X seconds? My roommate is like this. I would say because they have chosen the wrong language for this problem :-) Solving Sudoku is a typical finite domain constraint problem. Thus, a language with constraint solving facilities like Curry (a combination of Haskell and constraint logic programming) is much better suited. Actually, I wrote a Sudoku solver in Curry and the actual code for the solver is 10 lines of code which is compact and well readable (if you are familiar with Haskell), see http://www.informatik.uni-kiel.de/~curry/examples/CLP/sudoku.curry Regards, Michael

11 35

web servers
by Tim Newsham 15 Apr '06

15 Apr '06

Hi Everyone, I'm new to the list, been on irc a bit. I'm still learning haskell. Wanted to say Hi before getting in to things... I'm interested in real-world programs in haskell, especially ones where security and formal methods are important. I'm looking at web servers right now. I found a copy of Simon Marlow's HWS on haskell.org's cvs server. I know there's a newer plugin version, but I cant find a working link to the actual code. I've been able to get the code to compile after a while, but it still has some warnings of deprecated features which I havent been able to get rid of (if anyone's interested in helping out, let me know). Anyway, I configured it an ran it and it works, although I have noticed two security flaws in it which need fixing. Is it possible there is a newer version with these flaws fixed? Besides HWS, what other web servers exist? Does anyone actually use a haskell based web server in practice? Which web server is considered the most mature? stable? fastest? I'm trying to decided if I should sink some time into HWS or if I should use another server. Tim Newsham http://www.lava.net/~newsham/

6 7

6.2.1 for glibc-2.4
by Paul A. Steckler 15 Apr '06

15 Apr '06

I need a Linux ghc 6.2.1 built with glibc-2.4. The existing 6.2.1 RPM, built with glibc-2.3, works mostly OK, but with some programs, the generated executables barf and die on startup. Any suggestions on how to create such a beast? I've tried using ghc 6.4.1, for which there's a Fedora 5 RPM, to build 6.2.1 from source, but all sorts of compile errors occur. On a Linux with glibc-2.3 installed, is there a way to have the ghc build use a different glibc? -- Paul -- Paul Steckler, PhD Tel: +1 503.626.6616 x156 Galois Connections, Inc. Fax: +1 503.350.0833 12725 SW Millikan Way, Beaverton, OR 97005 Email: steck(a)galois.com

1 0

AFP 2006: any news ?
by Alain Cremieux 14 Apr '06

14 Apr '06

Hi, Has anyone any news about an Advanced Functional Programming school, which was scheduled for 2006 ? Thanks, Alain

2 1

RuntimeLoader
by Tim Newsham 14 Apr '06

14 Apr '06

Hi, I'm about to start playing with HWS-WP (web server + plugins). It relies on RuntimeLoader: http://www.algorithm.com.au/wiki/hacking/haskell.ghc_runtime_loading I grabbed the example and built it (only one minor tweak to imports to get it to build) but it doesnt quite work: $ ./src/TextFilter ./plugins/Lower.o < README TextFilter: ./plugins/Lower.o: unknown symbol `__stginit_Char_' TextFilter: user error (resolveFunctions failed?False) There were also some warnings during building: Compiling RuntimeLoader ( ../runtime_loader/RuntimeLoader.hs, ./RuntimeLoader .o ) /tmp/ghc11951.hc: In function `s2Pj_ret': /tmp/ghc11951.hc:170: warning: implicit declaration of function `unloadObj' /tmp/ghc11951.hc: In function `s2JU_entry': [...] I assume this is because it is mucking with some ghc internals? Is anyone familiar with this package? Is there a more up-to-date version or alternative? Tim Newsham http://www.lava.net/~newsham/

3 2

Local Fundeps [was: Fundeps: I feel dumb]
by oleg＠pobox.com 14 Apr '06

14 Apr '06

Creighton Hogg posed the following problem. Given a rather straightforward matrix multiplication code > -- The elements and the size > data Vec a = Vec (Array Int a) Int deriving (Show,Eq) > type Matrix a = (Vec (Vec a)) > class MatrixProduct a b c | a b -> c where > (<*>) :: a -> b -> c > instance (Num a) => MatrixProduct a (Vec a) (Vec a) where > (<*>) num (Vec a s) = Vec (fmap (*num) a) s > vector n elms = Vec (array (0,n-1) $ zip [0..n-1] elms) n we'd like to get the following straightforward test to compile: > test = 10 <*> (vector 10 [0..9]) The trouble it doesn't: the function (<*>) has the type a->b->c so the type of the scalar doesn't have to be in any a priori relation with the type of the matrix (to permit efficient representations for particular sorts of matrices). Such a general type for (<*>) means that the test expression does not constrain "10" to be of the same numeric type as the type of matrix elements. So, the inferred type for test is test :: (Num a, Num b, MatrixProduct a (Vec b) c) => c The constraint must be resolved (top level, monomorphism restriction): but it can't because there is no instance MatrixProduct a (Vec b) c There is only more specialized instance, which doesn't match. The solution exists: change test so that the type of the scalar and the base type of the vector are the same: > test1 = (10::Int) <*> (vector 10 [0..9::Int]) > test2 = let n = 10 in n <*> (vector 10 [0..(9 `asTypeOf` n)]) or add the type annotations in other ways. But that is annoying. Creighton Hogg asked if there is another way? There is. Change the instances to > instance (Num a,Num b,TypeCast a b) => MatrixProduct a (Vec b) (Vec b) where > (<*>) num (Vec a s) = Vec (fmap (* (typeCast num)) a) s The difference is subtle but important: given such a general instance, trying to resolve "MatrixProduct a (Vec b) c" now succeeds. Instance selection is done only based on the types in the head; constraints are not taken into account. When the match succeeds, GHC commits to it and goes checking the constraints. One of the constraints, TypeCast a b, says that the type a must be the same as b. Because 'a' and 'b' were just type variables (could be instantiated), that constraint succeeds and we accomplished our task. Now the original test types and works. In short: given the instance "C a a" and the constraint "C a b", we see failure: "C a a" can't match "C a b". The type variables of the latter aren't instantiated: this is matching, not the full unification. The re-written instance "TypeCast a b => C a b", effectively describes the same set of types. Now, however, "C a b" matches that instance -- and, the TypeCast constraint forces "a" and "b" to be the same. These _local_, per-instance functional dependencies notably improve the power of instance selection: from mere matching to some type improvement (towards the full unification). The net result is fewer type annotations required from the user. One might consider that useful. The full code: {-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-} module Foo where import Array data Vec a = Vec (Array Int a) Int deriving (Show,Eq) type Matrix a = (Vec (Vec a)) class MatrixProduct a b c | a b -> c where (<*>) :: a -> b -> c {- previously: instance (Num a) => MatrixProduct a (Vec a) (Vec a) where (<*>) num (Vec a s) = Vec (fmap (*num) a) s -} instance (Num a,Num b,TypeCast a b) => MatrixProduct a (Vec b) (Vec b) where (<*>) num (Vec a s) = Vec (fmap (* (typeCast num)) a) s vector n elms = Vec (array (0,n-1) $ zip [0..n-1] elms) n test = 10 <*> (vector 10 [0..9]) test1 = (10::Int) <*> (vector 10 [0..9::Int]) test2 = let n = 10 in n <*> (vector 10 [0..(9 `asTypeOf` n)]) class TypeCast a b | a -> b, b->a where typeCast :: a -> b class TypeCast' t a b | t a -> b, t b -> a where typeCast' :: t->a->b class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b instance TypeCast' () a b => TypeCast a b where typeCast x = typeCast' () x instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast'' instance TypeCast'' () a a where typeCast'' _ x = x

1 0

#if and #endif
by ihope 13 Apr '06

13 Apr '06

I grabbed the source code to Haddock, but GHC doesn't like the #if's and the #endif's. What can I do with these?

1 0

Re: [Haskell-cafe] Re: coherence when overlapping?
by Martin Sulzmann 13 Apr '06

13 Apr '06

I believe that GHC's overlapping instance extensions effectively uses inequalities. Why do you think that 'inequalities' model 'best-fit'? instance C Int -- (1) instance C a -- (2) under a 'best-fit' instance reduction strategy we would resolve C a by using (2). 'best-fit' should be very easy to implement. Simply order instances (resulting CHRs) in an appropriate 'best-fit' order. In case of instance C Int instance a =!=Int | C a (2') we can't reduce C a (because we can't satisfy a=!=Int) Notice that (2') translates to rule C a | a =!=Int <==> True I think it's better to write a =!=Int not as part of the instance context but write it as a guard constraint. I don't think there's any issue for an implementation (either using 'best-fit' or explicit inequalities). The hard part is to establish inference properties such as completeness etc. Martin Tom Schrijvers writes: > On Thu, 13 Apr 2006, Martin Sulzmann wrote: > > > > > Coherence (roughly) means that the program's semantics is independent > > of the program's typing. > > > > In case of your example below, I could type the program > > either use the first or the second instance (assuming > > g has type Int->Int). That's clearly bound. > > > > Guard constraints enforce that instances are non-overlapping. > > > > instance C Int > > instance C a | a =!= Int > > > > The second instance can only fire if a is different from Int. > > > > Non-overlapping instances are necessary but not sufficient to > > obtain coherence. We also need that types/programs are unambiguous. > > Claus Reinke was discussing this with me some time ago. He called it the > best fit principle, which would in a way, as you illustrate above, allow > inequality constraints to the instance head. You could even write it like: > > instance (a /= Int) => C a > > as you would do with the superclass constraints... I wonder whether > explicit inequality constraints would be useful on their own in all the > places where type class and equality constraints are used (class and > instance declarations, GADTs, ...). Or maybe it opens a whole new can of > worms :) > > Tom > > -- > Tom Schrijvers > > Department of Computer Science > K.U. Leuven > Celestijnenlaan 200A > B-3001 Heverlee > Belgium > > tel: +32 16 327544 > e-mail: tom.schrijvers(a)cs.kuleuven.be

4 3