Re: [Haskell] Specification and prover for Haskell
The Heterogeneous Tool Set supports HasCASL for specification of Haskell programs, and uses Isabelle for proving http://www.dfki.de/sks/hets Moreover, the Programatica project has an expressive logic called P-logic, and tools supporting it: http://programatica.cs.pdx.edu/ Best, Till Am 25.10.2010 10:09, schrieb Romain Demeyer: Hello, I'm working on static verification in Haskell, and I search for existing works on specification of Haskell programs (such as pre/post conditions, for example) or any other functional language. It would be great if there exists a prover based on this kind of specifications. I already found the ESC/Haskell. Do you know some other works which could be interesting? Thanks, rde. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] CfP: 20th WADT - deadline extended to May, 10th
[sorry if you receive this more than once] CALL FOR PAPERS DEADLINE FOR TWO-PAGE ABSTRACTS EXTENDED TO MAY, 10th WADT 2010 20th International Workshop on Algebraic Development Techniques July 1-4, 2010, Etelsen, Germany http://www.informatik.uni-bremen.de/WADT2010/ Aims and Scope: The algebraic approach to system specification encompasses many aspects of the formal design of software systems. Originally born as formal method for reasoning about abstract data types, it now covers new specification frameworks and programming paradigms (such as object-oriented, aspect-oriented, agent-oriented, logic and higher-order functional programming) as well as a wide range of application areas (including information systems, concurrent, distributed and mobile systems). The workshop will provide an opportunity to present recent and ongoing work, to meet colleagues, and to discuss new ideas and future trends. Topics of interest: Typical, but not exclusive topics of interest are: - Foundations of algebraic specification - Other approaches to formal specification, including process calculi and models of concurrent, distributed and mobile computing - Specification languages, methods, and environments - Semantics of conceptual modelling methods and techniques - Model-driven development - Graph transformations, term rewriting and proof systems - Integration of formal specification techniques - Formal testing and quality assurance, validation, and verification INVITED SPEAKERS Hans-Dieter Ehrich, Institut f\"ur Informationssysteme, Braunschweig Frantisek Plasil, Charles University, Prague Martin Wirsing, Ludwig-Maximilians-Universit\"at, M\"unchen IMPORTANT DATES Submission deadline for abstracts: May 10, 2010 Notification of acceptance: May 23, 2010 Final abstract due: June 13, 2010 Workshop:July 1-4, 2010 Workshop Format and Location: The workshop will take place over four days, Thursday to Sunday, at Schloss Etelsen, www.schloss-etelsen.de, a castle located near Bremen. Presentations will be selected on the basis of submitted abstracts. Three talks will be given by invited speakers. Submissions: The scientific program of the workshop will include presentations of recent results and ongoing research. The presentations will be selected by the Steering Committee on the basis of the submitted abstracts according to originality, significance, and general interest. The abstracts have to be submitted electronically according to the instructions published on the workshop web site. The final versions of the selected abstracts will be included in a hand-out for the workshop participants. After the workshop, selected authors will be invited to submit full papers for the refereed proceedings, which is expected to be published as a volume of Lecture Notes in Computer Science (Springer Verlag). Sponsorship: The workshop takes place under the auspices of IFIP WG 1.3, and is sponsored by IFIP TC1, University of Bremen, and DFKI GmbH. The event is organized by the Computer Science Department of the University of Bremen and the DFKI Bremen group Safe and Secure Cognitive Systems. WADT Steering Committee: Michel Bidoit(France) Andrea Corradini (Italy) Jos\'e Fiadeiro (UK) Rolf Hennicker (Germany) Hans-J\"org Kreowski (Germany) Till Mossakowski (Germany) [chair] Fernando Orejas (Spain) Francesco Parisi-Presicce(Italy) Andrzej Tarlecki (Poland) PROCEEDINGS The abstracts accepted for presentation will be available at the workshop. Refereed LNCS proceedings are planned for full versions of submissions solicited after the workshop. CONTACT WADT 2010 Fachbereich 3 Mathematik und Informatik Enrique-Schmidt-Str. 5 D-28359 Bremen, Germany Phone: +49 421 218 64226 Fax: +49 421 218 98 64226 Email: wadt2...@informatik.uni-bremen.de ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Call for Papers: 20th WADT (Workshop on Algebraic Development Techniques)
[sorry if you receive this more than once] CALL FOR PAPERS WADT 2010 20th International Workshop on Algebraic Development Techniques July 1-4, 2010, Etelsen, Germany http://www.informatik.uni-bremen.de/WADT2010/ Aims and Scope: The algebraic approach to system specification encompasses many aspects of the formal design of software systems. Originally born as formal method for reasoning about abstract data types, it now covers new specification frameworks and programming paradigms (such as object-oriented, aspect-oriented, agent-oriented, logic and higher-order functional programming) as well as a wide range of application areas (including information systems, concurrent, distributed and mobile systems). The workshop will provide an opportunity to present recent and ongoing work, to meet colleagues, and to discuss new ideas and future trends. Topics of interest: Typical, but not exclusive topics of interest are: - Foundations of algebraic specification - Other approaches to formal specification, including process calculi and models of concurrent, distributed and mobile computing - Specification languages, methods, and environments - Semantics of conceptual modelling methods and techniques - Model-driven development - Graph transformations, term rewriting and proof systems - Integration of formal specification techniques - Formal testing and quality assurance, validation, and verification INVITED SPEAKERS Hans-Dieter Ehrich, Institut f\"ur Informationssysteme, Braunschweig Frantisek Plasil, Charles University, Prague Martin Wirsing, Ludwig-Maximilians-Universit\"at, M\"unchen IMPORTANT DATES Submission deadline for abstracts: April 30, 2010 Notification of acceptance: May 23, 2010 Final abstract due: June 13, 2010 Workshop:July 1-4, 2010 Workshop Format and Location: The workshop will take place over four days, Thursday to Sunday, at Schloss Etelsen, www.schloss-etelsen.de, a castle located near Bremen. Presentations will be selected on the basis of submitted abstracts. Three talks will be given by invited speakers. Submissions: The scientific program of the workshop will include presentations of recent results and ongoing research. The presentations will be selected by the Steering Committee on the basis of the submitted abstracts according to originality, significance, and general interest. The abstracts have to be submitted electronically according to the instructions published on the workshop web site. The final versions of the selected abstracts will be included in a hand-out for the workshop participants. After the workshop, selected authors will be invited to submit full papers for the refereed proceedings, which is expected to be published as a volume of Lecture Notes in Computer Science (Springer Verlag). Sponsorship: The workshop takes place under the auspices of IFIP WG 1.3, and is sponsored by IFIP TC1, University of Bremen, and DFKI GmbH. The event is organized by the Computer Science Department of the University of Bremen and the DFKI Bremen group Safe and Secure Cognitive Systems. WADT Steering Committee: Michel Bidoit(France) Andrea Corradini (Italy) Jos\'e Fiadeiro (UK) Rolf Hennicker (Germany) Hans-J\"org Kreowski (Germany) Till Mossakowski (Germany) [chair] Fernando Orejas (Spain) Francesco Parisi-Presicce(Italy) Andrzej Tarlecki (Poland) PROCEEDINGS The abstracts accepted for presentation will be available at the workshop. Refereed LNCS proceedings are planned for full versions of submissions solicited after the workshop. CONTACT WADT 2010 Fachbereich 3 Mathematik und Informatik Enrique-Schmidt-Str. 5 D-28359 Bremen, Germany Phone: +49 421 218 64226 Fax: +49 421 218 98 64226 Email: wadt2...@informatik.uni-bremen.de ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] string type class
Sean Leather schrieb: Like this? http://hackage.haskell.org/cgi-bin/hackage-scripts/package/ListLike Indeed, a class StringLike is included there as well. Why not take or improve that one? Till ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Probably a trivial thing for people knowing Haskell
Chry Cheng schrieb: "Brandon S. Allbery KF8NH" <[EMAIL PROTECTED]> writes: Laziness is a double-edged sword. Perhaps the following page from Haskell Wiki would serve to enlighten more: http://haskell.org/haskellwiki/Foldr_Foldl_Foldl%27? This really made it clear to me how laziness can sometimes be a bad thing. A student of mine switch from Haskell to Java because of exactly these laziness problems - after he tried out to make the program stricter in various ways, but failed to remove the space leak. There should be an easy way of declaring a Haskell function (or, if that won't work, a whole module) to use strict evaluation only, without the need to manually insert seq and foldl' etc. everywhere (or even to change the structure of the code completely). Till Mossakowski ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Research position in spatial cogntion (Haskell-related)
1 Doctoral Research Assistant / Postdoctoral Researcher SFB/TR 8 project I4-[SPIN], Universität Bremen (TVL 13, approx. € 35,000 to € 50,000 p.a. gross) The research project I4-[SPIN] is concerned with classification and formalization of qualitative spatial calculi, relations among these calculi, spatial ontologies, and route graphs. Research tasks include both further development of the mathematical theory, the formalization and verification of critical results (like composition tables) using suitable specification languages and theorem proving tools, as well as further enhancement of these tools. The goal is to obtain both a trustworthy and efficient framework for qualitative spatial reasoning, which is applicable to reasoning tasks occurring in interactive wheelchair and robot navigation. The applicant should have a degree in computer science or in a related field (diploma, master's, or Ph.D.). Strong interest in formal methods and in interdisciplinary collaboration is expected. Especially, the applicant should have qualifications and/or interests in some of the following fields: . Qualitative spatial reasoning . Formal methods and theorem proving . Category theory . Functional programming (Haskell) We offer the opportunity to gain research experience in a modern and enthusiastic research environment with strong interdisciplinary and international links. Responsibilities include project work and research, publication of research results, supervision of student projects, participation in the activities of the SFB/TR 8, and contribution to research proposals. The position is available immediately / from January 2007 until the end of 2010. Extension is possible. Application deadline: 01 December 2006 (or until a suitable candidate is found). Universität Bremen is an equal opportunity employer. Women are especially encouraged to apply. Handicapped applicants with equal qualifications will be given preferential treatment. More information about this project can be found at www.sfbtr8.uni-bremen.de/i4. The Transregional Collaborative Research Center SFB/TR 8 Spatial Cognition: Reasoning, Action, Interaction at the Universities of Bremen and Freiburg, Germany pursues interdisciplinary long-term research in Spatial Cognition. Particular emphasis is given to: . Spatial Reasoning: Knowledge representation, human spatial thinking, computational modeling, diagrammatic reasoning, cognitive and computational complexity, qualitative spatio-temporal calculi; . Action in Space: Cognitive robotics, explorative localization and mapping, robot navigation, human navigation and wayfinding, sensorimotor representations of spatio-temporal structures, embodied cognition; . Communication and Interaction in Space: Formal methods, spatial and linguistic onto¬logies, computational linguistics, environmental cognition, integration of spatial methods. A description of the current research projects of the SFB/TR 8 can be found at www.sfbtr8.uni-bremen.de The SFB/TR 8 is funded by the German Research Foundation (DFG). Please address questions about the position and send your application (preferably by email) to: Dr. Till Mossakowski <[EMAIL PROTECTED]> SFB/TR 8 - Spatial Cognition Universität Bremen P.O. Box 330 440 28334 Bremen / Germany -- Till MossakowskiOffice: Phone +49-421-218-64226 DFKI Lab Bremen CartesiumFax +49-421-218-9864226 Robert-Hooke-Str. 5 Enrique-Schmidt-Str. 5 [EMAIL PROTECTED] D-28359 Bremen Room 2.051 http://www.tzi.de/~till ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Haskell XML
There is also the Haskell XML Toolbox (HXT) http://www.fh-wedel.de/~si/HXmlToolbox/ and HaXml http://www.cs.york.ac.uk/fp/HaXml/ Could someone summarize the pros and cons of HXT versus HaXml versus HSX? Greetings, Till Neil Mitchell schrieb: > Hi Greg, > > I've been using Haskell Source eXtensions which seems to have as much > XML language support as you could ever possibly need :) > > http://www.cs.chalmers.se/~d00nibro/haskell-src-exts/ > > Thanks > > Neil > > On 8/29/06, Lucius Meredith <[EMAIL PROTECTED]> wrote: >> All, >> >> Apologies if this question has been beaten to death, but i'm wondering if >> anyone out there has plans to do a language-level support for XML >> processing >> ala OCamlDuce. i would really like to be writing more code in Haskell, >> but >> XML is in almost everything i touch and OCamlDuce provides the right >> level >> of compiler support for the sorts of applications i'm writing. >> >> Best wishes, >> >> --greg >> >> -- >> L.G. Meredith >> Partner >> Biosimilarity LLC >> 505 N 72nd St >> Seattle, WA 98103 >> >> +1 206.650.3740 >> ___ >> Haskell mailing list >> Haskell@haskell.org >> http://www.haskell.org/mailman/listinfo/haskell >> >> >> > ___ > Haskell mailing list > Haskell@haskell.org > http://www.haskell.org/mailman/listinfo/haskell -- Till MossakowskiOffice: Phone +49-421-218-64226 DFKI Lab Bremen CartesiumFax +49-421-218-9864226 Robert-Hooke-Str. 5 Enrique-Schmidt-Str. [EMAIL PROTECTED] D-28359 Bremen Room 2.051 http://www.tzi.de/~till ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] translating Haskell into theorem provers
There is a prototype translation of Haskell to Isabelle/HOL and Isabelle/HOLCF written by Paolo Torrini. Unlike the Programatica translation, it uses a shallow encoding of the type system. Constructor classes (not available in Isabelle) are translated using theory morphisms. Programatica is used for parsing and type checking. The translation is part of the heterogeneous tool set (Hets) [1], but currently works only in a standalone version, called h2hf. You can compile h2hf from the Hets sources with "make h2hf". Since there is interest, we will provide a website with binaries, explanation and examples soon. Greetings, Till [1] http://www.tzi.de/cofi/hets Gerwin Klein wrote: Hi, is any of you aware of activities that aim to translate Haskell into interactive theorem provers like PVS or Isabelle/HOL? (automatically or manually). We know about the Programatica project and Brian Huffman's work, but turned up little else. Cheers, Gerwin ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen [EMAIL PROTECTED] P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] duplicate elements in Data.Set
The problem probably is that your Ord instance does not define a total order. Below a small example exhibiting the same problem. This shows the usefulness of specification of Haskell programs (e.g. with Programatica or HasCASL) - verification could be used to detect such problems. Till module SetExample where import Data.Set data D = A | B | C deriving (Eq, Show) instance Ord D where compare A B = LT compare _ _ = GT l = fromList [A,B,C,A,B,C] main = putStrLn (show (valid l)) Walter Moreira wrote: Hello list. Are there situations where a set can contain duplicate elements? I have a newtype and it is an instance of 'Eq' via the 'compare' method, and it is also an instance of 'Ord'. After some Data.Set operations with sets of that type I get a set which contains two elements which compare equal. What am I doing wrong? The function 'Set.valid' returns 'False' when applied to the set. I use the function 'Set.fromList' sometimes. Is it supposed to always yield a valid set? or it may depend on the order or equality? Sorry the question is a little vague. When I try to construct small examples the problem disappear. Thanks, Walter ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen [EMAIL PROTECTED] P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Making Haskell more open
I have also made nice experiences with MediaWiki/WikiPedia. However, I think while you can include images on MediaWiki pages, you cannot include documents (like ps or pdf) - these have to be external links. Of course, the possibility of including such documents would be a desirable feature for a system of Haskell documentation pages. Perhaps it is not too difficult to add this feature for a MediaWiki expert? Till Mossakowski Andrea Sassanelli wrote: Sorry to intrude myslf like this in the conversation. First of all, let me present myself: My name is Andrea Sassanelli, and I'm Italian. I have just started studying Haskell at the UoEdinburgh this year, and immediatelly fell in love with it. On a sidenote, the wikipedia does rely on moderators who review the changes, but common users are able to undo changes as well, and can therefore bring a maliciously messed up page back to it's origiinal state. Basically MediaWiki/WikiPedia rely on the assumption that there are more good folk than bad folk, and this (IMHO) should be even more true in the case of a relatvelly "medium/small-scale" thing like the Haskell Documentation (small compared to a whole encyclopedia, i mean). Open documentation like this is definitelly a good idea to make the language docs not only more accessible, but also more user-friendly, and would surely give a positive image to the community as a whole. I unfortunatelly am not suted (?yet?) to work on any usefull documentation, as I am a novice, but I think the system would work. Andrea Sassanelli ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen [EMAIL PROTECTED] P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] formal verification for functional programming languages
Wolfgang Jeltsch wrote: Hello, where can I find information about formal verification techniques and tools for functional programming languages? Both introductionary texts and current research papers etc. are welcome. See the specification language HasCASL. For specification of monadic programs, we have developed a Hoare calculus and a dynamic logic, which are also represented in the theorem prover Isabelle. Related is the Heterogeneous Tool Set. http://www.tzi.de/agbkb/forschung/formal_methods/CoFI/HasCASL/ http://www.tzi.de/cofi/hets The Isabelle tutorial has some examples from functional programming http://www4.in.tum.de/~nipkow/LNCS2283/ Also, P-logic and the Programatica tool should be of interest: ftp://ftp.cse.ogi.edu/pub/pacsoft/papers/Plogic.pdf http://www.cse.ogi.edu/PacSoft/projects/programatica/ Greetings, Till -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen [EMAIL PROTECTED] P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: ST/STRef vs. IO/IORef
Remi Turk wrote: Ah, I think I understand what we're disagreeing about exactly now. We're understanding "primitive" to mean different things :) You're seeing runST, newSTRef, writeSTRef etc as primitives, is that correct? I see them as the public interface to something which is implemented in something else. The advantage of seeing runST, newSTRef, writeSTRef etc as primitives is that there is a denotational semantics for them (see Laucnbury/ Peyton Jones: "State in Haskell"), which coincides with the operational semantics. This is not the case for unsafePerformIO. unsafePerformIO is a purely operational primitive, although some uses of unsafePerformIO can a posteriori (and usually with a lot of handwaving) shown to behave in a good (denotational) way. The ghc file you cite should be regarded as operational detail, not as a language definition of runST, newSTRef, and writeSTRef. Remi "We're probably agreeing 99.9% anyway" Turk Yes, of course. Till -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen [EMAIL PROTECTED] P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: ST/STRef vs. IO/IORef
Bulat Ziganshin wrote: Hello Till, Friday, August 05, 2005, 10:04:53 AM, you wrote: TM>MonadState IOArray IOArray ST TM>withwith with TM>FiniteMap unsafePerformIO MutArr TM> safe yesyes noyes TM> efficient no yes yes yes afaik, ST efficient only with small enough arrays. one time i tried STArray of about 100 000 elements and seen that things goes much worse than in IO monad with IOArray. on small arrays STArray performs good enough (i was trying to create sorting routine. afair, it was an insert sort) That is weird, because in base/GHC/IOBase.lhs, IOArray is constructed on top of STArray: newtype IOArray i e = IOArray (STArray RealWorld i e) But maybe ghc has some special treatment of IOArray. Till -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen [EMAIL PROTECTED] P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: ST/STRef vs. IO/IORef
Remi Turk wrote: In a final attempt to convince someone of I'm not exactly sure what, I attached a simple implementation of the ST monad in terms of unsafePerformIO + IORef + IOArray. OK, but you have to reason about this implementation to show that it is safe (which may be difficult because unsafePerformIO makes reasoning extremely difficult), while the primitives of ST are more easily proved to be safe. -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen [EMAIL PROTECTED] P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: ST/STRef vs. IO/IORef
Sebastian Sylvan wrote: On 8/4/05, Till Mossakowski <[EMAIL PROTECTED]> wrote: Remi Turk wrote: MonadState needs multi-parameter type classes, State and StateT don't. And ST needs rank-2 types (or at least one rank-2 constant) and, to be implemented _efficiently_, also needs something like unsafePerformIO (or even lower-level unsafe mutable state primitives). I think one could call the ST monad a safe yet still efficient variant of unsafePerformIO + IORef's + IOArray's. No, the point of ST is that it is safe (as opposed to unsafePerformIO), but still has the advantages of being both efficient and allowing purely functional encapsulation via runST (as oppesed to IORefs and IOArrays). The only price is that you need rank-2 polymorphism and new language primitives for creating, reading and writing references. But using these primitives is much better than using unsafePerformIO - the latter entails a lot of harmful things. Hmmm... Wasn't that what he said? I disagree with the equation "primitives = unsafe" that is implicit in sentence to be implemented _efficiently_, also needs something like unsafePerformIO (or even lower-level unsafe mutable state primitives). The point is that ST uses *safe* primitives, and not "something like unsafePerformIO". To clarify things, here a little table about different possibilities of using arrays in Haskell: MonadState IOArray IOArray ST withwith with FiniteMap unsafePerformIO MutArr safe yesyes noyes efficient no yes yes yes allows yesno yes yes functional encapsulation avoids yesno nono in-place- update primitives avoids yes yes yes no rank 2 -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen [EMAIL PROTECTED] P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: ST/STRef vs. IO/IORef
Remi Turk wrote: MonadState needs multi-parameter type classes, State and StateT don't. And ST needs rank-2 types (or at least one rank-2 constant) and, to be implemented _efficiently_, also needs something like unsafePerformIO (or even lower-level unsafe mutable state primitives). I think one could call the ST monad a safe yet still efficient variant of unsafePerformIO + IORef's + IOArray's. No, the point of ST is that it is safe (as opposed to unsafePerformIO), but still has the advantages of being both efficient and allowing purely functional encapsulation via runST (as oppesed to IORefs and IOArrays). The only price is that you need rank-2 polymorphism and new language primitives for creating, reading and writing references. But using these primitives is much better than using unsafePerformIO - the latter entails a lot of harmful things. -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen [EMAIL PROTECTED] P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] translation of "kind"
Wolfgang Jeltsch wrote: Am Samstag, 18. Juni 2005 20:25 schrieben Sie: can anybody tell me what the German translation of the word "kind" as used in type theory and especially in Haskell is? Wie wär's mit `Sorte', Ralf I have already thought about that but was not sure it was correct since the meaning of "Sorte" in algebra is very different from what is meant with "kind" in type theory. This confusion is already present within the English language: the theorem prover Isabelle uses the English term "sort" for what in Haskell is called "kind", while in the context of universal algebra, "sort" means what in Haskell is called (basic) "type". Hence "sort" and "Sorte" perhaps should be avoided entirely. -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen [EMAIL PROTECTED] P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Type of y f = f . f
The name y suggests that you want to define the fixpoint combinator. This works as follows: Prelude> let y f = f (y f) Prelude> :type y y :: forall t. (t -> t) -> t Prelude> y (\fac n -> if n == 0 then 1 else n*fac(n-1)) 10 3628800 Prelude> Till Pedro Vasconcelos wrote: On Mon, 28 Feb 2005 03:50:14 -0500 Jim Apple <[EMAIL PROTECTED]> wrote: Is there a type we can give to y f = f . f y id y head y fst are all typeable? Using ghci: Prelude> let y f = f.f Prelude> :t y y :: forall c. (c -> c) -> c -> c So it admits principal type (a->a) -> a->a. From this you can see that (y head) and (y fst) cannot be typed, whereas (y id) can. BTW, this function is usually named 'twice'. Best regards, Pedro -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen [EMAIL PROTECTED] P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Semantics of Haskell
My statement was just: There are several papers on the semantics of Haskell, but none of these papers treats recursive datatypes. I am looking for a treatment of the semantics of recursive datatypes in Haskell, preferably by translation to known meta-languages like FPC or system F. Till Keean Schupke wrote: When I looked through several papers about Haskell semantics, I found that recursive datatypes have been omitted. I believe fairly strong reasons have been given why this would be a bad thing, and would result in problems for type-inference. Haskell has iso-revursive types, which if defined using the 'newtype' directive should have no run-time cost. Keean. -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen [EMAIL PROTECTED] P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Semantics of Haskell
When I looked through several papers about Haskell semantics, I found that recursive datatypes have been omitted. Is there a denotational semantics of Haskell including recursive datatypes? (or better some translation into a meta-language that has a denotational semantics) More precisely, (1) is there a translation of Haskell without polymorphism into FPC? It should be rather straightforward, but is it written down somewhere? (2) a translation of Haskell with polymorphism, polymorphic recursion, higher-rank polymorphism, into (some extension of) system F? Till Mossakowski -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen [EMAIL PROTECTED] P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Syntax of functional dependencies
I errorneously specified categories as class (Eq object, Eq morphism) => Category id object morphism | id ->, id -> morphism where o :: id -> morphism -> morphism -> Maybe morphism dom, cod :: id -> morphism -> object it should have been class (Eq object, Eq morphism) => Category id object morphism | id -> object, id -> morphism ... ^^ - but ghci 5.02.2 does not complain. Why? Till Mossakowski -- Till MossakowskiPhone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen[EMAIL PROTECTED] P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: multiparameter generic classes
We are using multiparameter classes with fundeps in the project MULTIPLE, which is about heterogeneous specification in multi-logic frameworks. See http://www.tzi.de/cofi/projects/multiple.html The interesting challenge is not only genericity (over an arbitray logic), but also heterogeneity (i.e. coexistence and communication of several logics, coded as instances of the multiparameter class). A paper describing the implementation is not available yet, but in preparation. Till Mossakowski > are there any papers/webpages/implementations/etc. of using multiparameter > classes in a generic framework, with or without dependencies? > > thanks! > > - hal > > -- > Hal Daume III -- Till MossakowskiPhone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen[EMAIL PROTECTED] P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Sockets and firewalls
Hello, I have seen that there are several Haskell libraries for cgi scripts and the like. Is there also a possibiliy to deal with sockets and firewalls? Till Mossakowski -- Till MossakowskiPhone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen[EMAIL PROTECTED] P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Research assistant positions in Bremen
The following two research assistant positions are available at the University of Bremen, Germany. The Bremen Institute of Safe Systems in the Center for Computing Technologies at the University of Bremen hosts the research projects "Multi-logic systems as a basis for heterogeneous specification and development" (MULTIPLE) and "Algebraic specification + functional programming = environment for formal software development" (HasCASL) funded by the Deutsche Forschungsgemeinschaft (DFG). Within the framework of each of these projects, one position in the working group of Prof. Dr. Krieg-Brückner is to be immediately filled for at least two years (additional option for another two years), subject to availability of funds: Research Assistant Verg. Gr. IIa BAT (full time) In addition to successful university studies in computer science, experience and skills in functional programming (e.g. Haskell, ML) are expected. Familiarity with at least one of formal specification methods (like CoFI/CASL), theorem proving or category theory is desirable. Applicants with a PhD are welcome. However, there will also be the oppurtunity to prepare a PhD thesis in connection with the research project. In case of essentially equal qualification in the subject and personal suitability, severely handicapped applicants will be preferred. The University of Bremen intends to increase the share of women in scientific activities and does therefore strongly encourage women to apply for these positions. More detailed information about the projects can be found under http://www.tzi.de/cofi/projects/multiple.html http://www.tzi.de/cofi/projects/hascasl.html Please address your application with the usual documents and the reference number A164/00 (MULTIPLE) resp. A165/00 (HasCASL) before 01.02.2001 to: UNIVERSITÄT BREMEN Prof. Dr. B. Krieg-Brückner Fachbereich 3 Postfach 33 04 40 28334 Bremen e-Mail: [EMAIL PROTECTED] -- Till MossakowskiPhone: +49-421-218-4683, monday: +49-4252-1859 Dept. of Computer Science Fax: +49-421-218-3054 University of BremenEMail: [EMAIL PROTECTED] P.O.Box 330440, D-28334 Bremen WWW: http://www.tzi.de/~till ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
