March 2001 - Haskell - Haskell.org

CALL FOR PAPERS -- JOURNAL OF FUNCTIONAL PROGRAMMING
by Simon Helsen 07 Mar '01

07 Mar '01

CALL FOR PAPERS SPECIAL ISSUE JOURNAL OF FUNCTIONAL PROGRAMMING: DEPENDENT TYPE THEORY MEETS PROGRAMMING PRACTICE Modern programming languages rely on advanced type systems that detect errors at compile-time. While the benefits of type systems have long been recognized, there are some areas where the standard systems in programming languages are not expressive enough. Language designers usually trade expressiveness for decidability of the type system. Some interesting programs will always be rejected (despite their semantical soundness) or be assigned uninformative types. There are several remedies to this situation. Dependent type systems, which allow the formation of types that explicitly depend on other types or values, are one of the most promising approaches. These systems are well-investigated from a theoretical point of view by logicians and type theorists. For example, dependent types are used in proof assistants to implement various logics and there are sophisticated proof editors for developing programs in a dependently typed language. To the present day, the impact of these developments on practical programming has been small, partially because of the level of sophistication of these systems and of their type checkers. Only recently, there have been efforts to integrate dependent systems into intermediate languages in compilers and programming languages. Additional uses have been identified in high-profile applications such as mobile code security, where terms of a dependently typed lambda calculus to encode safety proofs. A special issue of the Journal of Functional Programming will be devoted to the interplay between dependent type theory and programming practice. We welcome technical contributions in the field, as well as position papers that: - make researchers in programming languages aware of new developments and research directions on the theory side; - point out to theorists practical uses of advanced type systems and urge them to address theoretical problems arising in emerging applications. Authors who are concerned about the appropriateness of a topic are welcome to contact the guest editors. Manuscripts should be unpublished works and not submitted elsewhere. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are eligible for submission. All submissions will be reviewed according to the usual standards of scholarship and originality. Submissions should be sent to Gilles Barthe (Gilles.Barthe(a)inria.fr) with a copy to Nasreen Ahmad (nasreen(a)dcs.gla.ac.uk) Submitted articles should be sent in postscript format preferably gzipped and uuencoded. In addition, please send, as plain text, title, abstract, and contact information. The submission deadline is December 1st, 2001. Guest Editors: o Gilles Barthe, INRIA Sophia-Antipolis, France o Peter Dybjer, Chalmers Tekniska Högskola, Sweden o Peter Thiemann, Universität Freiburg, Germany

1 0

GHC - Cygwin Installation and also DirectX
by Mike Thomas 07 Mar '01

07 Mar '01

Hi all. I'm having ghc import path problems on NT: ---------------------------------------------------------------------------- ------------------------------ $ ghc -i//c/ghc/ghc-4.08.2/lib/imports/win32 hello.lhs Import path element `/cygdrive/c/ghc/ghc-4.08.2/lib/imports/win32' does not exist, ignor ing. hello.lhs:14: Could not find interface file for `Win32' in the directories /cygdrive/c/ghc/ghc-4.08.2/lib/imports/win32/*.hi ./*.hi C:/ghc/ghc-4.08.2/lib/imports/std/*.hi hello.lhs:15: Could not find interface file for `Addr' in the directories /cygdrive/c/ghc/ghc-4.08.2/lib/imports/win32/*.hi ./*.hi C:/ghc/ghc-4.08.2/lib/imports/std/*.hi Compilation had errors ---------------------------------------------------------------------------- ------------------------------ The Win32 installation instructions say that one should execute "mount -f C: /", but having done that in response to this error it does not fix the problem and it stops bash from starting up correctly (Cygwin is installed in c:\cygwin and GHC in c:\ghc\ghc-4.08.2). (Why am I supposed to do this mount?) Has anyone got a solution? Furthermore, is anyone using Direct X especially Direct Play and Draw with GHC? Cheers Mike Thomas.

4 3

Re: Viewing inferred types
by Bernard James POPE 07 Mar '01

07 Mar '01

I think that the ability to view types of subexpressions in programs would be very useful. Some work has been done in this direction. One example I know of is Typeview (www-users.cs.york.ac.uk/~olaf/PUBLICATIONS/typeview.html) The last time I checked it only worked for a small functional language. > Focusing on part 1, I see two possible approaches: > > A. Ask an existing Haskell interpreter/compiler to output the > information. I looked briefly at the implementations listed at > http://www.haskell.org; none of them seems to produce anything > (i.e., any debugging output) from which the necessary information > can be extracted. Therefore, to take this approach, we would need > to modify an implementation. I would be very happy to be > corrected on this observation. I have looked at pulling types out of various compilers. This can be tricky for a number of reasons. ghc provides the -ddump-types flag which will dump type signatures for all top-level bindings in a module. With some help from the devlopers I was able to get types for local bindings as well (lets and wheres). Still, with this information you would need to do some reconstruction of subexpression types within your typeviewer. nhc98 provides the option -tbound, which shows the symbol table after type checking. If I remember correctly I had trouble with the renamer of nhc98. It seemed hard to reconcile source ids with their renamed counterparts. > B. Connect a Haskell parser (e.g., hsparser) to a Haskell type > checker (e.g., _Typing Haskell in Haskell_). This is the > preferred approach because the solution would not depend on the > internals of any Haskell implementation. However, the output of > hsparser is neither typed nor desugared for piping into _Typing > hsparser is neither typed nor desugared for piping into _Typing > Haskell in Haskell_, so some conversion/desugaring work is > required. I am nearly finished doing precisely this task. Basically I have stuck hsparser onto the front of thih (with a lot of glue). It only works for single module programs at the moment, and it runs slowly. The reason I did this is that I need detailed type information for some other work that I am doing, and I couldn't easily get what I wanted from the compilers. It is not currently available for public release, partly because it needs some polishing, and partly because not all of the code is mine to release (some of it is Mark Jones'). The intention is to make an alpha release available soon (next few weeks) with the appropriate permissions granted of course. A colleague of mine will be speeding up the code and adding better error diagnostics, and time permitting, extending the code to multi-modules (possibly with a hmake style front-end). If you want more information, or you wish to collaborate on this project please let me know. Bernie

1 0

Viewing inferred types
by Ken Shan 06 Mar '01

06 Mar '01

Hello all, When I edit Haskell code in a text editor, I often want to point at an expression and be told its type. (Even assuming that this feature only works when the entire file type-checks correctly, it would still be very useful to me.) For example, in let c:cs = "string" in ... I would like to point at "c" and be told that c :: Char c:cs :: [Char] I divide this functionality into two parts: 1. Given a Haskell program, produce a list of pairs (span, type), where "span" is a contiguous region in the source code that parses as an expression, and "type" is the type of the expression (possibly universally quantified and/or with context). 2. Make this information easy to generate and view in an editor. Focusing on part 1, I see two possible approaches: A. Ask an existing Haskell interpreter/compiler to output the information. I looked briefly at the implementations listed at http://www.haskell.org; none of them seems to produce anything (i.e., any debugging output) from which the necessary information can be extracted. Therefore, to take this approach, we would need to modify an implementation. I would be very happy to be corrected on this observation. B. Connect a Haskell parser (e.g., hsparser) to a Haskell type checker (e.g., _Typing Haskell in Haskell_). This is the preferred approach because the solution would not depend on the internals of any Haskell implementation. However, the output of hsparser is neither typed nor desugared for piping into _Typing Haskell in Haskell_, so some conversion/desugaring work is required. I would appreciate any comments, pointers to existing work, or other help on this project. In particular, how much work would be involved in approach B above, and has it already been done? Thanks in advance! -- Edit this signature at http://rodimus.digitas.harvard.edu/cgi-bin/ken/sig Dumpster Clocking: The tendency when looking at objects to guesstimate the amount of time they will take to eventually decompose: "Ski boots are the worst. Solid plastic. They'll be around till the sun goes supernova."

1 0

Re: Can Class do this?
by Saswat Anand 06 Mar '01

06 Mar '01

Thanks a lot. It works great with Hugs. But it has a small problem. I also want to be able to write 4 \+ fc :: CF fc \+ 4 :: CF ic \+ 4 :: IF 4 \+ fc \+ ic :: CIF Well for that I did this, instance (Rational a) => Plus a CF CF where --to support 4.0 \+ fc f \+ g = \c -> (realToFrac f) \+ (g c) I did not do : instance Plus Float CF CF where .. so that I don't have to write (4::Float) \+ fc. But it complains because, it violates functional dependency a b -> c. Is there any other way to avoid writing (4::Float) in this case. Well I tried this: (\+) :: (Lift a c, Lift b c) => a -> b -> (c -> Float) f \+ g = \x -> (lift f) x + (lift f) x class Lift a b where lift :: a -> (b -> Float) instance Lift CF Char where lift = id instance Lift CF (Char,Integer) where lift f = \(c,i) -> f c instance Lift IF Integer where lift = id instance Lift IF (Char,Integer) where lift f = \(c,i) -> f i instance Lift CIF (Char,Integer) where lift = id But it does not take following: x :: CF x = cf \+ cf \+ cf Cannot justify constraints in explicitly typed binding *****Expresssion : x *****Type : CF *****Given Context : () *****Constraints : (Lift (a -> Float) Char, Lift (Char -> FLoat) a) Thanks, Saswat

2 1

Can Class do this?
by Saswat Anand 06 Mar '01

06 Mar '01

I have a problem as follows - type CF = Char -> Float type IF = Integer -> Float type CIF = (Char,Integer) -> Float There be two functions: fun :: CF fun = fromInt.ord sun :: IF sun = fromInteger I want the followings to be valid. x :: IF x = sun \+ sun y :: IF y = sun \+ sun \+ sun -- when only sun is there, type should be IF a :: CF a = fun \+ fun b :: CF b = fun \+ fun \+ fun -- when only fun is there, type should be IF p :: CIF p = sun \+ fun q :: CIF q = sun \+ fun \+ sun - -when sun and fun are mixed type should be CIF I guess this can be done using classes, but I have not been successful after trying many variations. Any help is very much appreciated. Thanks, Saswat

2 1

Re: Extensible Algebraic Data Types
by cwitty＠newtonlabs.com 05 Mar '01

05 Mar '01

Ashley Yakeley <ashley(a)semantic.org> writes: > I think it would be useful to extend Haskell so that one could create > algebraic data types in one module that could be union-extended in > another. Something like this: > > data Thing = CharThing Char | IntThing Int | _ > > ...later... > > data Thing |= StringThing String You might be able to use the Gaster and Jones extensible variants from "A Polymorphic Type System for Extensible Records and Variants" (http://www.cse.ogi.edu/~mpj/pubs/polyrec.html) As far as I know, the extensible variants described in this paper have never been implemented (although the extensible records are implemented in Hugs). I've often thought that extensible variants would be at least as useful, if not more useful, than extensible records. Carl Witty

1 0

Disjoint type classes
by Jose Emilio Labra Gayo 05 Mar '01

05 Mar '01

I have a large program where I would like to include disjoint type classes into a new type class. My problem can be reduced to the following example (taken from [1]): > class Num a => Dividable a > where dividedBy :: a -> a -> a > instance Fractional a => Dividable a where > dividedBy = (/) > instance Integral a => Dividable a where > dividedBy = div Which doesn't work because Haskell doesn't detect that "Integral" and "Fractional" are disjoint. Is there a way to implement these type classes with current Haskell implementations? [1] K. Glynn, M. Sulzmann, P.J. Stuckey Type Classes and Constraint Handling Rules http://www.cs.mu.oz.au/tr_submit/test/cover_db/mu_TR_2000_7.html Best regards, Jose Labra

2 1

Rewrite rules
by Simon Peyton-Jones 05 Mar '01

05 Mar '01

Folks Andrew Tolmach, Tony Hoare, and I are writing a paper about rewrite rules in GHC -- the {-# RULES #-} stuff. We'd like to report on practical experience of using rewrite rules. Has anyone use them in practice? What's your experience? Pls reply to me, to avoid clogging the list with your cries of rapture. Simon

1 0

RE: question re hugs and func dependencies
by Simon Peyton-Jones 05 Mar '01

05 Mar '01

I replied last week: -----Original Message----- From: Simon Peyton-Jones Sent: 28 February 2001 16:51 To: 'Dominic Duggan'; hugs-bugs(a)haskell.org Subject: RE: please confirm that this is a feature GHC infers the type g :: (Foo [[a]] [b], Foo [[b]] [a]) => [a] -> [b] -> Int As you imply, if GHC used the instance decl to simplify the first constraint to Foo [a] b, for example, then the functional dependency would kick in, and there would be an infinite loop. But GHC's constraint simplification is (now) lazy, unless forced to be eager by supplying a type signature. I think Hugs is the same, and I think that's probably why it terminates. Interesting example! Simon | -----Original Message----- | From: Dominic Duggan [mailto:dduggan@cs.stevens-tech.edu] | Sent: 02 March 2001 21:55 | To: haskell(a)haskell.org | Subject: question re hugs and func dependencies | | | Dear all, I haven't got a reply from hugs-bugs, | so I'll see if anyone here can answer the question. | | class foo a b | a |-> b where foo :: a -> b -> Int | instance foo Int Float where foo x y = 0 | instance foo [a] [b] where foo [x] [y] = foo x y | g x y = (foo [x] y) + (foo [y] x) | | It is my conjecture that Hugs terminates on type-checking | g because of a depth bound in the type-checker | (although there is no indication from the type-checker | that this is what is going on). | | Can anyone confirm or refute this conjecture? | | FWIW this is as part of the related work section | for a paper that has been accepted to JFP: | "Type-Checking Multi-Parameter Type Classes," | by D. Duggan and J. Ophel. | | I'd appreciate cc-ing any replies to me, I'm not | sure that I'm still on this mailing list. | | Cheers | --dd |

2 1