August 2003 - Haskell

The madness of implicit parameters: cured?
by Ben Rudiak-Gould 05 Aug '03

05 Aug '03

When I first learned about implicit parameters I thought they were a great idea. The honeymoon ended about the time I wrote some code of the form "let ?foo = 123 in expr2", where expr2 used ?foo implicitly, and debugging eventually unearthed the fact that ?foo's implicit value was not being set to 123 in expr2. That was enough to scare me off of using implicit parameters permanently. More recently, I've realized that I really don't understand implicit parameters at all. They seemed simple enough at first, but when I look at an expression like f x = let g y = ?foo in g I realize that I have no idea what f's type should be. Is it (?foo :: c) => a -> b -> c or is it a -> ((?foo :: c) => b -> c) ? As far as I can tell, these are not the same type: you can distinguish between them by partially applying f with various different values of ?foo in the implicit environment. GHC tells me that f has the former type, but I still have no idea why: is it because g has an implicit ?foo parameter and f implicitly applies its own ?foo to g before returning it? Why would it do that? Or is it because ?foo is here interpreted as referring to an implicit parameter bound in the call of f, instead of in g? That doesn't make sense either. The final straw was: Prelude> let ?x = 1 in let g = ?x in let ?x = 2 in g 1 Prelude> let ?x = 1 in let g () = ?x in let ?x = 2 in g () 2 This is insanity. I can't possibly use a language feature which behaves in such a non-orthogonal way. Now the interesting part: I think I've managed to fix these problems. I'm afraid that my solution will turn out to be just as unimplementable as my original file I/O proposal, and that's very likely in this case since I'm far from grokking Haskell's type system. So I'm going to present my idea and let the gurus on this list tell me where I went wrong. Here we go. First, discard the current implicit-parameter scheme entirely. (I'll eventually build up to something very similar.) Now introduce the idea of "explicit named parameters" to Haskell. This requires three extensions: a new kind of abstraction, a new kind of application, and a way of representing the resulting types. The abstraction could be done with a new lambda form, but instead I'll use a special prefix on identifiers which are to be considered named parameters, namely the character #. The new application form will be [F] { #x = [G] } where [F] and [G] are expressions. [F] must evaluate to a function with an explicit named parameter #x. The type notation for a named parameter will be (#name :: type). They can appear only on the left side of a ->. Named parameters can only be passed by name, so their order relative to positional parameters and each other doesn't matter; therefore we may as well "bubble them up" to the head of the list of arguments. In fact, we could put them in the context with the type classes, but I won't do so. Examples: cons :: (#elem :: a) -> (#list :: [a]) -> [a] cons #elem #list = #elem : #list cons { #elem = 'h', #list = "ello" } -- legal cons 'h' "ello" -- illegal: named params must be passed by name cons { #list = "ello" } -- legal, has type (#elem :: Char) -> String cons { #list = "ello", #elem = 'h' } -- legal cons { #list = "ello" } { #elem = 'h' } -- legal append :: (#right :: [a]) -> [a] -> [a] append left #right = ... -- named args gravitate left Now introduce the idea of "auto-lifted named parameters". I'll distinguish these from ordinary named parameters by using an @ prefix instead of #. These are exactly the same as ordinary named parameters except that if they appear in the type on the right hand side of an application node, they are implicitly lifted to the whole node. For example, if [F] has an auto-lifted parameter @p, and [G] has auto-lifted parameters @p and @q, then [F][G] is implicitly converted to something like \@p @q -> [F] { @p = @p } ( [G] { @p = @p, @q = @q } ). Finally, introduce the following syntax: * As an expression, ?x is short for \@x -> @x. * On the left hand side of the = sign in a named application, ?x is the same as @x. * For backward compatibility, "let ?x = [E] in [F]" should be treated as equivalent to "[F] { ?x = [E] }". Now we have something almost the same as the current implicit-parameter system, except that it behaves in a much safer and saner way. For example, looking at the confusing expressions from the beginning again: f x = let g y = ?foo in g This obviously has type (?foo :: c) -> a -> b -> c. It doesn't matter where the ?foo parameter appears in the type because it will always be referred to explicitly, by name, exactly once in each call of f. let ?x = 1 in let g = ?x in let ?x = 2 in g This reduces as follows: let ?x = 1 in let g = ?x in let ?x = 2 in g ( let g = \@x -> @x in g { @x = 2 } ) { @x = 1 } (\@x -> @x) { @x = 2 } { @x = 1 } 2 { @x = 1 } At this point we get a type error, as we should: a let binding of an implicit parameter that's never used is almost certainly a coding error. let ?x = 1 in let g () = ?x in let ?x = 2 in g () Reduces in exactly the same way as the previous case, with the same result. Again, this is as is should be. Why are the semantics so much clearer? I think the fundamental problem with the existing semantics is the presence of an implicit parameter environment, from which values are scooped and plugged into functions at hard-to-predict times. By substituting a notation which clearly means "I want this implicit parameter of this function bound to this value right now, and if you can't do it I want a static type error", we avoid this ambiguity. More thoughts, assuming this all pans out (knocking on wood): * Explicit named parameters seem like a useful idea too. Maybe they should be added to Haskell. * We should really, really drop the "let ?x" form and switch to the record-update notation. In "( let g = ?x in g { ?x = 2 } ) { ?x = 1 }" it's obvious what's going to happen and what the result will be, but in "let ?x = 1 in let g = ?x in let ?x = 2 in g" it's very unclear, even though, under the translation above, these two forms are equivalent. * I think it may be possible to extend this to provide default values for named parameters, which would be really really cool (no more separate foo and fooBy functions). -- Ben

4 14

Re: The madness of implicit parameters: cured?
by Ashley Yakeley 05 Aug '03

05 Aug '03

At 2003-08-04 20:00, Ben Rudiak-Gould wrote: >This is a different lambda calculus, with a different beta rule. You can >see the same effect in the type inference rules for implicit parameters: >If f has type Int -> String and ?x has type (?x :: Int) => Int, then f ?x >has type (?x :: Int) => String, i.e. the implicit ?x parameter is lifted >out of the RHS to become a parameter of the whole application node. This >rule is what makes implicit parameters implicit. Ah. Actually I think the beta rule is unchanged with Haskell's implicit parameters. Consider: x :: (?x :: Int) => Int f :: Int -> String f :: ((?x :: Int) => Int) -> ((?x :: Int) => String) -- specialisation f x :: (?x :: Int) => String -- apply beta rule >As you pointed out, this reduction behavior depends on f's type, so this >is necessarily a typed lambda calculus. But that's okay because Haskell is >statically typed. So is this valid or not? b :: (?x :: Int) => Int b = \@x -> @x f :: ((?x :: Int) => Int) -> (Int,Int) f = \a -> ((a,\@x -> @x) {@x = 2}) f b :: (Int,Int) f b = ((b,\@x -> @x) {@x = 2}) = ((\@x -> @x,\@x -> @x) {@x = 2}) If it is valid, then this must be a valid reduction: ((\a -> ((a,\@x -> @x) {@x = 2})) (\@x -> @x),\@x -> @x) {@x = 1} ((\@x -> @x,\@x -> @x) {@x = 2},\@x -> @x) {@x = 1} -- Ashley Yakeley, Seattle WA

2 1

Pure functional TypeRep [Was: Existentials...]
by oleg＠pobox.com 05 Aug '03

05 Aug '03

This message shows how to map _types_ to integers at compile time -- and then extend this facility to run-time so it can be used with existentially-quantified types. It is statically guaranteed that different types receive different integer labels. Unlike TyCons of Dynamics, our mapping does NOT rely on unsafePerformIO. We use the typechecker itself to compare types. It seems our typemap can also be used for _safe_ casts, in particular, for casting away the existential blemish. This message was inspired by Amr Sabry's problem on existentials. Unlike Hal Daume's solution posted here earlier, we do not use Dynamics nor GMap -- therefore, we completely avoid unsafePerformIO and unsafeCoerce. Our solution is purely functional and assuredly type-safe (to the extent the typechecker can be trusted). Extensions used: -fglasgow-exts -fallow-undecidable-instances -fallow-overlapping-instances First, the compile-time mapping from types to integers. Polytypic list: > data Nil t r = Nil > data Cons t r = Cons t r > > class PList ntype vtype cdrtype where > cdr:: ntype vtype cdrtype -> cdrtype > empty:: ntype vtype cdrtype -> Bool > value:: ntype vtype cdrtype -> vtype > > instance PList Nil vtype cdrtype where > empty = const True > > instance (PList n v r) => PList Cons v' (n v r) where > empty = const False > value (Cons v r) = v > cdr (Cons v r) = r and the finite map from types to integers > class TypeSeq t s where > type_index:: t -> s -> Int > > instance (PList Cons t r) => TypeSeq t (Cons t r) where > type_index _ _ = 0 > > instance (PList Cons t' r', TypeSeq t r') => TypeSeq t (Cons t' r') where > type_index v s = 1 + (type_index v $ cdr s) Let us build some finite map > init_typeseq = Cons (undefined::Char) $ > Cons (undefined::Int) $ > Cons (undefined::Bool) $ > Cons (undefined::String) $ > Cons (undefined::Maybe Char) $ > Nil A typeseq maps a type to an integer -- which is the type's position in the polytypic list. We are satisfied with the first occurrence of the type in the list. It is plain that a typeseq maps different types to different integers. Let us see how it works: -- *Main> type_index True init_typeseq -- 2 -- *Main> type_index 'a' init_typeseq -- 0 -- *Main> type_index "a" init_typeseq -- 3 -- *Main> type_index (1::Int) init_typeseq -- 1 -- *Main> type_index (Just 'a') init_typeseq -- 4 -- *Main> type_index (Just True) init_typeseq -- <interactive>:1: -- No instance for (TypeSeq (Maybe Bool) (Nil t r)) -- arising from use of `type_index' at <interactive>:1 -- In the definition of `it': type_index (Just True) init_typeseq We call this mapping compile-time because the translation from a type to the corresponding encoding (1+1+...1) is done at compile time, when the appropriate instance of the TypeSeq class is chosen. A sufficiently smart compiler can just as well fold the constant expression (1+1...+1) down to a single integer. Also, errors in the translation are reported at compile-time. However, to apply the mapping to existential types, we need to extend the former to run-time. > class TypeRep t where > tr_index:: t -> Int > > -- All of the following are almost the same. > -- The Template Haskell can really help us here > instance TypeRep Char where > tr_index x = type_index x init_typeseq > > instance TypeRep Int where > tr_index x = type_index x init_typeseq > > instance TypeRep Bool where > tr_index x = type_index x init_typeseq > > instance TypeRep String where > tr_index x = type_index x init_typeseq > > instance TypeRep (Maybe Char) where > tr_index x = type_index x init_typeseq Now, Amr Sabry's Problem > data F a b = > forall c. (TypeRep c) => PushF (a -> c) (F c b) > | Bottom (a -> b) > > f1 :: Char -> Bool > f1 'a' = True > f1 _ = False > > f2 :: Bool -> String > f2 True = "true" > f2 False = "false" > > f3 :: String -> Int > f3 = length > > fs = PushF f1 (PushF f2 (PushF f3 (Bottom id))) First, we make fs an instance of class Show. It is jolly convenient. > data HF = forall a b. (TypeRep a,TypeRep b) => HF (F a b) > show_fn_type (g::(a->b)) > = "(" ++ (show (tr_index (undefined::a))) ++ > "->"++(show (tr_index (undefined::b))) ++ ")" > > instance (TypeRep a, TypeRep b) => Show (F a b) where > show = show . hsf_to_lst . HF > where > hsf_to_lst (HF (Bottom g)) = [show_fn_type g] > hsf_to_lst (HF (PushF g next)) = (show_fn_type g):(hsf_to_lst$HF next) Now, Amr Sabry's question: ] Is it possible to write a function ] f :: F a b -> T c -> F c b ] where (T c) is some type for values of type 'c' or values representing ] the type 'c' or whatever is appropriate. Thus if given the ] representation of Bool, the function should return: ] PushF f2 (PushF f3 (Bottom id)) ] and if given the representation of String the function should return ] PushF f3 (Bottom id) ] and so on. First, we prepend to the given F a b structure the identity composition. We see the meaning of it below. > f fs v = f' (PushF id fs) v > f':: (TypeRep c) => (F a b) -> c -> F a b > f' here@(PushF g next) (v::tv) = > if tr_index v == tr_index (g undefined) > then here > else case next of > PushF g1 next' -> f' (PushF (g1.g) next') v > Bottom g1 -> f' (Bottom (g1.g)) v The function f' takes a data structure F a b and a value of type c and returns another data structure F a b, but of a different structure PushF g next here 'next' has the type F c b -- which is the answer to Amr Sambry's question. The function g::a->c is a composition of all previously occurring functions. This is a neat "side-effect" of the function f': we partially compose the given F a b structure up to the given type. Let us see how it works: *Main> fs ["(0->2)","(2->3)","(3->1)","(1->1)"] *Main> f fs 'a' ["(0->0)","(0->2)","(2->3)","(3->1)","(1->1)"] *Main> f fs True ["(0->2)","(2->3)","(3->1)","(1->1)"] *Main> f fs "a" ["(0->3)","(3->1)","(1->1)"] *Main> f fs (1::Int) ["(0->1)","(1->1)"] Because f is capable of producing any partial composition, it can do the full composition just as easily: > flatten:: (TypeRep a, TypeRep b) => F a b -> (a -> b) > flatten fs :: (a->b) > = case f fs (undefined::b) of > PushF g (Bottom g1) -> g1.g And it indeed works: *Main> flatten fs 'a' 4 -- the length of the word true *Main> flatten fs 'b' 5 -- the length of the word false Again, I can't seem to write any Haskell code that doesn't explicitly use undefined.

4 8

Re: The madness of implicit parameters: cured?
by Ashley Yakeley 05 Aug '03

05 Aug '03

At 2003-08-04 18:19, Ben Rudiak-Gould wrote: > \@x -> ((\a -> ((a,\@x -> @x) {@x = 2})) @x) > >If we next apply (\a -> ...) to @x, something interesting happens: we >have to rename to avoid variable capture. I don't see why, isn't this much the same as ordinary names? (\a -> ((\a -> a) 1,a)) 2 ((\a -> a) 1,2) (1,2) -- Ashley Yakeley, Seattle WA

1 0

Re: The madness of implicit parameters: cured?
by Ashley Yakeley 05 Aug '03

05 Aug '03

At 2003-08-04 18:19, Ben Rudiak-Gould wrote: >> ((\a -> ((a,\@x -> @x) {@x = 2})) (\@x -> @x),\@x -> @x) {@x = 1} > ^^^ >> ((\@x -> @x,\@x -> @x) {@x = 2},\@x -> @x) {@x = 1} > >This reduction is incorrect. It's a simple beta-reduction, it must be correct. b :: (?x :: Int) => Int b = \@x -> @x f :: ((?x :: Int) => Int) -> (Int,Int) f = \a -> ((a,\@x -> @x) {@x = 2}) f b :: (Int,Int) f b = ((b,\@x -> @x) {@x = 2}) -- Ashley Yakeley, Seattle WA

2 1

Re: The madness of implicit parameters: cured?
by Ashley Yakeley 05 Aug '03

05 Aug '03

At 2003-08-03 14:09, Ben Rudiak-Gould wrote: >This reduction is incorrect. Auto-lifted parameters on the RHS of an >application get lifted out I am interpreting this as "Auto-lifted parameters on the RHS of an application get lifted out before {@x=y}-style 'beta'-reduction can be done". I think this is ambiguous: ((\a -> ((a,?x) {@x = 2})) ?x,?x) {@x = 1} ((\a -> ((a,\@x -> @x) {@x = 2})) (\@x -> @x),\@x -> @x) {@x = 1} 1. ((\@x -> @x,\@x -> @x) {@x = 2},\@x -> @x) {@x = 1} ((\@x -> (@x,@x)) {@x = 2},\@x -> @x) {@x = 1} ((2,2),\@x -> @x) {@x = 1} (\@x -> ((2,2),@x)) {@x = 1} ((2,2),1) 2. (\@x -> ((\a -> ((a,\@x -> @x) {@x = 2})) @x,@x)) {@x = 1} ((\a -> ((a,\@x -> @x) {@x = 2})) 1,1) (((1,\@x -> @x) {@x = 2}),1) (((\@x -> (1,@x)) {@x = 2}),1) ((1,2),1) A simpler query: what types can f have here? Which if any should the compiler infer? f a b = (a,b) {@x = 2} And given that type, which of these are valid? f ?x ?x f ?x 1 f 1 ?x f 1 1 -- Ashley Yakeley, Seattle WA

2 1

haskell for educative games
by Andre W B Furtado 04 Aug '03

04 Aug '03

Does anyone know if Haskell is/was used to develop educative games? Do you recommend some papers on the subject? Thanks a lot, -- Andre Furtado

2 1

ANNOUNCE: GHC version 6.0.1
by Simon Marlow 04 Aug '03

04 Aug '03

============================================================= The (Interactive) Glasgow Haskell Compiler -- version 6.0.1 ============================================================= We are pleased to announce a new patchlevel release of the Glasgow Haskell Compiler (GHC), version 6.0.1. This is a bug-fix release relative to 6.0. The most important bugfixes are: * Fixes to make GHC work with GCC 3.3 * Fix for the "GHC deletes source files" bug * :cd now unloads any loaded modules in GHCi. * -mk-dll should work better on Windows. in addition to various other bugfixes. The release notes lists the changes in the 6.0 line relative to 5.04: http://www.haskell.org/ghc/docs/latest/html/users_guide/release-6-0.html How to get it ~~~~~~~~~~~~~ The easy way is to go to the WWW page, which should be self-explanatory: http://www.haskell.org/ghc/ We supply binary builds in the native package format for various flavours of Linux and BSD, and in Windows Installer (MSI) form for Windows folks. Binary builds for other platforms are available as a .tar.gz which can be installed wherever you want. The source distribution is also available from the same place. Packages will appear as they are built - if the package for your system isn't available yet, please try again later. Background ~~~~~~~~~~ Haskell is a standard lazy functional programming language; the current language version is Haskell 98, agreed in December 1998, and revised in December 2002. GHC is a state-of-the-art programming suite for Haskell. Included is an optimising compiler generating good code for a variety of platforms, together with an interactive system for convenient, quick development. The distribution includes space and time profiling facilities, a large collection of libraries, and support for various language extensions, including concurrency, exceptions, and foreign language interfaces (C, whatever). GHC is distributed under a BSD-style open source license. A wide variety of Haskell related resources (tutorials, libraries, specifications, documentation, compilers, interpreters, references, contact information, links to research groups) are available from the Haskell home page (see below). On-line GHC-related resources ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Relevant URLs on the World-Wide Web: GHC home page http://www.haskell.org/ghc/ Haskell home page http://www.haskell.org/ comp.lang.functional FAQ http://www.cs.nott.ac.uk/~gmh/faq.html System requirements ~~~~~~~~~~~~~~~~~~~ To compile programs with GHC, you need a machine with 64+MB memory, GCC and perl. This release is known to work on the following platforms: * i386-unknown-{linux,*bsd,mingw32} * sparc-sun-solaris2 * alpha-dec-osf3 * powerpc-apple-darwin (Mac OS X) Ports to the following platforms should be relatively easy (for a wunderhacker), but haven't been tested due to lack of time/hardware: * hppa1.1-hp-hpux{9,10} * i386-unknown-solaris2 * mips-sgi-irix{5,6} * {rs6000,powerpc}-ibm-aix The builder's guide on the web site gives a complete run-down of what ports work; it can be found at http://www.haskell.org/ghc/docs/latest/html/building/building-guide.html Mailing lists ~~~~~~~~~~~~~ We run mailing lists for GHC users and bug reports; to subscribe, use the web interfaces at http://www.haskell.org/mailman/listinfo/glasgow-haskell-users http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs There are several other haskell and ghc-related mailing lists on www.haskell.org; for the full list, see http://www.haskell.org/mailman/listinfo/ Please report bugs using our SourceForge page at http://sourceforge.net/projects/ghc/ or send them to glasgow-haskell-bugs(a)haskell.org. GHC users hang out on glasgow-haskell-users(a)haskell.org. Bleeding edge CVS users party on cvs-ghc(a)haskell.org.

5 4

Re: The madness of implicit parameters: cured?
by Ashley Yakeley 04 Aug '03

04 Aug '03

At 2003-08-03 14:09, Ben Rudiak-Gould wrote: >> ((let g = \_ _ -> \@x -> @x in ((g (\@x -> @x)) {@x = 2})) (\@x -> >> @x)){@x = 1} >> ((let g = \_ _ -> \@x -> @x in (g 2)) (\@x -> @x)){@x = 1} > >This reduction is incorrect. Auto-lifted parameters on the RHS of an >application get lifted out, so > > g (\@x -> @x) => (\@x -> g { @x = @x } @x) Hmm... I assume you mean specifically this: g (\@x -> @x) \@x -> (g { @x = @x } @x) Supposing you have this: g = \_ -> 3 then you have this reduction: g ?x g (\@x -> @x) \@x -> (g { @x = @x } @x) \@x -> ((\_ -> 3) { @x = @x } @x) error: can't apply (\_ -> 3) { @x = @x } Something else I haven't mentioned is that you shouldn't use (->) as such in the type signatures. This is because (->) is an ordinary type-constructor. For instance, if you define this: type Func = (->) then all these are the same type: Func a b (->) a b a -> b But in your scheme, (->) has been extended to allow certain pseudo-types in its first position. It might be better to use a different syntax rather than overload (->) with something that isn't a type-constructor. -- Ashley Yakeley, Seattle WA

2 1

ANN: H98 FFI Addendum 1.0, Release Candidate 12
by Manuel M T Chakravarty 04 Aug '03

04 Aug '03

Dear Haskell Folks, Release Candidate 12 of the H98 FFI Addendum 1.0 is now available from http://www.cse.unsw.edu.au/~chak/haskell/ffi/ Since the release of RC 11 (12 June), there was only one small change (which was already under discussion before RC 11 was published). Hence, I consider Version 1.0 of the FFI Addendum to be completed; no changes except linguistic ones and plain error corrections will be accepted anymore for this version. Cheers, Manuel -=- Changes since RC11: * 5.5: Swapped argument order of `newForeignPtr' and `addForeignPtrFinalizer' Note to FFI people, there were at least three votes (Alastair, Sven, and me) for this change and none against.

4 5