April 2004 - Haskell - Haskell.org

UNIF'04 workshop @ IJCAR 2004: First Call for Papers
by Michael Kohlhase 26 Apr '04

26 Apr '04

[ Apologies for multiple copies which are unavoidable. -Michael. ] First Call for Papers/Abstracts/System descriptions UNIF 2004 18th International Workshop on Unification July 4-5, 2004, Cork, Ireland Affiliated with IJCAR'04 http://www.faculty.iu-bremen.de/mkohlhase/event/unif04/ UNIF is the main international meeting on unification. Unification is concerned with the problem of identifying given terms, either syntactically or modulo a given logical theory. Syntactic unification is the basic operation of most automated reasoning systems, and unification modulo theories can be used, for instance, to build in special equational theories into theorem provers. The aim of UNIF 2004, as that of the previous meetings, is to to bring together people interested in unification, present recent (even unfinished) work, and discuss new ideas and trends in unification and related fields. In particular, it is intended to offer a good opportunity for young researches and researchers working in related areas to get an overview of the current state of the art in unification theory and get in contact with the experts in the field. ---------------------------------------------------------------------- TOPICS OF INTEREST ---------------------------------------------------------------------- A non-exclusive list of topics of interest is: * Unification * E-unification * Unification Algorithms * Higher-Order Unification * String Unification * Context Unification * Combination problems * Disunification * Typed Unification * Related Topics * Constraint Solving * Tree Descriptions * Matching * Narrowing * Applications * Type Checking and Type Inference * Automated Deduction * Rewriting * Functional and Logic Programming * Grammars * Computational Linguistics * Implementations ---------------------------------------------------------------------- INVITED SPEAKERS ---------------------------------------------------------------------- There will be two invited speakers. ---------------------------------------------------------------------- IMPORTANT DATES ---------------------------------------------------------------------- Deadline for electronic submission: Friday, May 14, 2004 Email: unif04(a)iu-bremen.de Notification of acceptance: Monday, May 24, 2004 Deadline for camera-ready papers: Monday, June 7, 2004 Workshop: July 4 - 5, 2004 ---------------------------------------------------------------------- SUBMISSION DETAILS ---------------------------------------------------------------------- Authors are invited to submit via email an abstract (1-5 pages), a paper (no longer than 15 pages), or a system description (no more than 5 pages) in Postscript or PDF format to: unif04(a)iu-bremen.de before May 14, 2004. Authors are encouraged to use LaTeX2e and the Springer llncs class. ---------------------------------------------------------------------- PUBLICATION ---------------------------------------------------------------------- Accepted papers, abstracts and system descriptions will be included in the proceedings which will be available at the workshop. ---------------------------------------------------------------------- ORGANIZING COMMITTEE ---------------------------------------------------------------------- Michael Kohlhase (International University Bremen, Germany) Hitoschi Ohsaki (National Institute of Advanced Industrial Science and Technology, Amagasaki, Japan) Steve Prestwich (Universtity College, Cork, Ireland) Ralf Treinen (Ecole Normale Superieure, Cachan, France) Manfred Schmidt-Schauss (Johann Wolfgang Goethe-Universit"at Frankfurt am Main, Germany) -- ------------------------------------------------------------------------- Prof. Dr. Michael Kohlhase, Office: Research 1, Room 62 Professor for Computer Science Campus Ring 12, School of Engineering & Science D-28758 Bremen, Germany International University Bremen tel/fax: +49 421 200 3140/3103 http://www.cs.cmu.edu/~kohlhase e-mail: <m.kohlhase(a)iu-bremen.de> --------------------------------------------------------------------------

1 0

a newbie question
by Ben_Yu＠asc.aon.com 26 Apr '04

26 Apr '04

Hi there. I got this question while I'm messing around with my toy monad. I was thinking about creating a generic monad that can persist state change even when fail is called. The StateT monad will discard the state change so it makes it hard to add tracing to the program. (at least to me. If there's any nice way of doing this, please kindly instruct me.) Then I come to this problem. I can summarize it by removing all irrelavant stuff like this: to_write :: ((x->a)->r) -> (x->(a,s)) -> (r,s) to_write f1 f2 = ... how do I implement it? I can't get a data of type x, so the only way is to pass f2 into f1. In order to pass f2 to f1, I have to discard the s returned by f2. Thus, I lose the s forever. Hope I'm getter myself clear. Any comment is welcome. Ben.

3 2

WSC9 - Call for Papers
by Ajith Abraham 25 Apr '04

25 Apr '04

** WSC9 - Call for Papers *** ### FREE ONLINE CONFERENCE ### WSC9: 9th Online World Conference on Soft Computing in Industrial Applications September 20th - October 08th, 2004 ** On the World Wide Web ** Conference URL: http://www.cs.nmt.edu/~wsc9/ Mirror: http://wsc9.softcomputing.net/ General Information about WSC9: Original papers and tutorials are invited for the 9th Online World Conference on Soft Computing in Industrial Applications (WSC9) to be held on the Internet. WSC9 aims at bringing together outstanding research and developments in the field of soft computing (evolutionary computation, fuzzy logic, neural networks, and their fusion) and its applications across the world with the goal to publish high-quality research quickly and with less cost. Accepted papers of WSC9 will be published as an edited volume by Springer Verlag, Germany after the conference. Moreover, extended versions of selected papers of the conference will also be invited for a "fast track" submission for the Elsevier Science Applied Soft Computing Journal. We aim to have inspiring discussions between the authors and participants, and make them visible to everyone on the Internet. There will be a number of mirror sites around the world to make easier the access to this major event. Please note that the registration is open to everyone and it is completely free of charge. June 04th, 2004 Deadline for submissions of regular papers, online survey paper proposals and online tutorial proposals. Papers are submitted in electronic form as PDF-files through the conference web site. Authors are also encouraged to submit multi-media demonstrations (including software etc.) July 30th, 2004 Acceptance/rejection notification August 27th, 2004 Submission of full papers and online presentations September 20th - October 08th, 2004 Online conference November 12th, 2004 Submission of camera-ready papers for final review Topics of Interest: Submissions are invited in, but not limited to, any of the following areas: Soft Computing for Modeling, Control, and Optimization Fuzzy Control Neuro-Fuzzy Systems Genetic Fuzzy Systems Neuro-Fuzzy-Genetic Systems Software Agent Systems and Architectures Multi-Agent Architectures and Collaborative Learning Ant Colony Optimization Fuzzy Information Fusion Rough Sets Bayesian Networks Fuzzy Image Processing Bio-inspired Systems Artificial Neural Networks Support Vector Machines Evolutionary Algorithms, Simulated Annealing, Tabu Search Evolutionary Multiobjective Optimization Hybrid Optimization Techniques (integration of global search and local search techniques) Simulation Environments Data Mining Industrial Applications of Soft Computing Intelligent Information Retrieval Language Processing Robotics Autonomous Reasoning Fault Diagnosis Bioinformatics Web Intelligence Speech Processing Business Information Systems Knowledge Management Paper Submission Authors should fill up the online form and upload a full paper (max. 10 pages) in PDF format by June 04, 2004. Authors who are interested to submit a paper should send an expression of interest to: <wsc9(a)softcomputing.net> including title of paper and author details. Organized session proposals and tutorials are welcome. Please notify the Special Events Chair, Katrin Franke (katrin.franke(a)ipk.fhg.de) about your intention to organize a session/tutorial as soon as possible. For special sessions, please send session title, organizer’s name and e-mail address, a short synopsis of session objective (max. 100 words), organizer's expertise in the field, and a tentative list of papers in the proposed technical session. At least three session papers have to be submitted by June 04, 2004. For online proposals and survey papers, please send the abstract and biography of the presenter before June 04, 2004 and if approved send the final presentation paper by August 27th, 2004. Paper Acceptance: All accepted papers would be presented during the online conference. Participants are also encouraged to present multimedia presentations like online demonstrations, software, video clips etc.) to make the online discussions more interesting. Authors of accepted papers have to register and visit the conference website on a regular basis in order to respond to questions and comments on their paper without delay. By November 26th, 2004, camera-ready copies of extended papers have to be submitted for final inclusion in the conference proceedings. Significantly revised and enhanced versions of selected papers of the conference will also be invited for a "fast track" submission for the Applied Soft Computing Journal. WSC 9 Organization Honorary Chair Ronald Yager, Iona College, USA General Chair Ajith Abraham, Oklahoma State University, USA Program Chair Mario Köppen, Fraunhofer IPK Berlin, Germany International Co-chairs Frank Hoffmann, University of Dortmund, Germany Avineri Erel, Ben-Gurion University of the Negev, Israel Sponsorship Chair Rajkumar Roy, University of Cranfield, UK Publication Chair Bernard de Baets, Ghent University, Belgium Virtual Exhibition Chair Fabio Zambetta, University of Bari, Italy Special Events Chair Katrin Franke, Fraunhofer IPK Berlin, Germany Industrial Liason Chairs Antony Satyadas, IBM, USA Suthikshn Kumar, Larsen & Toubro Infotech, India Best Paper Award Chair Janos Abonyi, University of Veszprém, Hungary International Technical Program Committee Walter D. Potter, University of Georgia, USA Mark Embrechts, Rensselaer Polytechnic Institute, USA Hisao Ishibuchi, Osaka Prefecture University, Japan Thomas Sudcamp, Wright State University, USA Christian Wöhler, Daimler Chrysler AG, Germany Vasile Palade, Oxford University, UK Marley Vellasco, University College London, UK Yaochu Jin, Honda Research Institute Europe, Germany Yukinori Suzuki, Muroran Institute of Techology, Japan John Debanham, University of Technology Sydney, Australia Yanqing Zhang, Georgia State University, USA Srinivasan S.H., Satyam Computers, India Okyay Kaynak , Bogazici University, Turkey Hung T. Nguyen, New Mexico State University, USA Aureli Soria Frisch, FhG IPK Berlin, Germany Jae C. Oh, Syracuse University, USA Andrea Bonarini, Politecnico di Milano, Italy Andreas Koenig, University of Kaiserslautern, Germany Bart Baesens, Katholieke Universiteit Leuven, Belgium Brian Carse, University of the West of England, UK Christophe Marsala, University Pierre et Marie Curie Paris, France Detlef D. Nauck, BTexact Technologies Ipswich, UK Francisco Herrera, E.T.S. Ingeneria Informatica Granada, Spain Frank Klawonn, University of Applied Sciences Braunschweig/Wolfen, Germany Guy de TrÈ, Ghent University, Belgium Hani Abdel Kader Hagras, University of Essex, UK Javier Ruiz-del-Solar, Universidad de Chile, Chile Leandro dos Santos Coelho, Pontificia Universidade Catolica do Paran Curitib, Brazil Luis Magdalena, Ciudad Universitaria Madrid, Spain Mauro Dell'Orco, Polytechnic of Bari, Italy Sankar Kumar Pal, Indian Statistical Institute Kolkata, India SenÈn Barro Ameneiro, SEVIMAV Santiago de Compostela, Spain Vicent Torra, Universitat AutÚnoma de Barcelona, Spain Takeshi Furuhashi, Mie University, Japan Oscar Cordon, University of Granada, Spain Vitorino Ramos, CRVM IST, Portugal P. Saratchandran, Nanyang Technological University, Singapore Sonja Petrovic-Lazarevic, Monash University, Australia Andew Sung, New Mexico Institute of Mining and Technology, USA Zaheeruddin, Jamia Milia Islamia New Dehli, India Xiao-Zhi Gao, Helsinki University of Technology, Finland Edward Tunstel, NASA, USA Berend Jan van der Zwaag, University of Twente, The Netherlands Muhammad Sarfraz, King Fahd University of Petroleum and Minerals, Saudi Arabia ------------------------------------------------ Please address all general enquiries to <wsc9(a)softcomputing.net>

1 0

Re: [Haskell] Correct interpretation of the curry-howard isomorphism
by Bruno Oliveira 24 Apr '04

24 Apr '04

Hi! Thanks Connor, I enjoyed your answer, it was very illustrative. >> but then, it would be too easy to write this in haskell: >> >> coerce :: a -> b >> coerce x = undefined >> >> As an obvious consequence, Haskell type system would be unsound. >> >> So, I assumed that this would be a wrong interpretation. >This is the part of your email which frightens me the most. Of >course Haskell's type system is unsound! What factors lead you to >this kind of assumption? Clearly a misconception of mine. Is it a good excuse that people told me that (or I misunderstood them) :) ? >The type system does not become a logic until you populate some of >the types (hopefully only those corresponding to true propositions) >with the terms which describe the construction of proofs. You can't >pretend that Haskell is sound just by hoping that Curry and Howard >(when properly interpreted) won't be able to see the broken bits. >It's nonetheless an interesting question which bits you need to >throw away to get a sound language. You'll have to get rid of > y :: (p -> p) -> p > unJust :: Maybe wmd -> wmd >and hence the programming language features which enable them to >be constructed, in particular, pattern matching with incomplete >coverings, and general recursion. Yes, I thought about those implications, that's why I also thought (incorrectly) that it would be too limiting and therefore probably wrongly interpreted. It is also, not too hard to see, as you said, that general recursion would validate that interpretation (even without using any other primitives or functions): coerce :: a -> b coerce = coerce or even coerce :: a -> b coerce x = let y = y in y Then, even if we ignored the primitives, Haskell would still be unsound! Moreover, we could then say that most of the functional languages (which have a similar type system) are unsound. Right ? Is it "Charity" an exception on this? >There's an interesting paper `Elementary Strong Functional >Programming' by David Turner, in which he proposes such a language. >He suggests that, at least for paedagogical purposes, a functional >language which gave up completeness for consistency might be no >bad thing. I'm inclined to agree with him. I will take a look on it. >So I won't make any foolish and portentous pronouncements about >dependent types being the only way to save us from damnation. I'll >merely observe that we often use the unsound parts of programming >languages as the best approximations available to the programs >we really mean: we don't intend recursion to loop infinitely, >we just have no means to explain in the program why it doesn't; >we don't intend to apply unJust to Nothing, we just have no means >to explain in the program why this can't happen. Dependent types >support a higher level of articulacy about what is really going on, >reducing, but not removing entirely the need to work outside the >consistent fragment of the language. They do not save us from Satan >but from Wittgenstein. Whereon you know something, thereon speak! Dependent types definitely seem an advance to me. I saw recently a presentation of a very impressive tool (epigram - I wonder if you have heard about it :P). I'll be definitely take a better look on it as soon as I finish some work with more priority. Best Regards, Bruno

6 6

RE: [Haskell] Why is newChan in the IO Monad?
by Nick Benton 23 Apr '04

23 Apr '04

Double is a pretty poor choice of "whatever" (just thinking about equality of floating point numbers puts one in a state of sin :-)). Worse still, your newChanSafe would be type-unsafe if you gave it that polymorphic type (think about it). So let's assume channels aren't polymorphic and that we were were going to use ints or strings or something as identities. Then since your newChan has got to be injective, you could just identify chan with int and be done with it. Even then, there's still quite a lot going on: Firstly, of course, the equation I wrote *does* actually hold in Haskell with the current definitions. But it would fail to hold if newchan were a non-normal form, each evaluation of which returned a new name, which was what was intended. Secondly, if you manage your own channel identities you'll end up carrying around a "current" identity/name supply and having an operation which takes a supply and gives you a fresh name and a new supply. That's just another monad (TX = supply->X*supply, gensym : Tname). If the type you use for names isn't abstract (e.g. you just use int) then the resulting equational theory will be weak (because contexts can supply all the names). A more refined treatment is possible. If (and only if) you make the type of names and their operations more abstract then there is a very nice monad just for name generation, which you could separate from the monad for actually sending and receiving values. One advantage of doing that is that the dynamic allocation monad satisfies more equations than the IO monad (it's commutative, for example). Then there's a monad morphism that lets you lift new name generation into the IO monad when you want to use the channels (IO is definitely not commutative). If you want to do fancy program transformations then this extra refinement is helpful. If you don't, having two monads instead of one just makes life even more complicated. Now, giving newChan a non-monadic type amounts to making this new name monad *implicit* - allowing divergence and/or name-generation to happen during evaluation without reflecting either possibility in the types. As I said, this breaks the equational theory of the language. But other people have taken the position that maybe it doesn't break it all that badly, and that one can make sure that the compiler's transformations respect the weaker theory [1]. This is what happens in "observable sharing", which was suggested precisely because others, like you, found doing gensym monadically in Haskell to be a bit tedious: K. Claessen and D. Sands. Observable sharing for functional circuit description. In ASIAN'99, volume 1742 of Lecture Notes in Computer Science, pages 62--73. Springer-Verlag, 1999. Names in circuit descriptions are used to express the sharing which distinguishes cyclic circuits from infinite ones. In the case of channels, however, you don't just compare the names for equality - all non-trivial uses of them are going to involve sends and receives and hence put you into the IO monad anyway. So messing up the theory of the whole language just to to have a few fewer IOs doesn't seem a good tradeoff. If you're interested in the theory, there's a big (and rapidly growing!) literature on the semantics of name generation - see the work of Pitts & Stark on the \nu-calculus, for example. To summarize the above ramble: it's an excellent question, but you almost certainly want to leave newChan where it is. Nick [1] arguably, including strict constructs (pattern matching, strict sequencing) is already a step down this road. But the Haskell/Miranda "war of the bottoms" was all a long time ago... -----Original Message----- From: S. Alexander Jacobson [mailto:alex@alexjacobson.com] Sent: 23 April 2004 20:05 To: Nick Benton Cc: Haskell Mailing List Subject: RE: [Haskell] Why is newChan in the IO Monad? Yes, that makes sense, but I'm ok with passing in an identity. I'd like a function like this: newChanSafe::Identity -> Chan a type Identity = Double -- or whatever -Alex- _________________________________________________________________ S. Alexander Jacobson mailto:me@alexjacobson.com tel:917-770-6565 http://alexjacobson.com On Fri, 23 Apr 2004, Nick Benton wrote: > Channels have identity, so allocating a new one is a side effecting > operation. Having it outside the IO monad would require (for example): > > (newChan, newChan) = (let x = newChan in (x,x)) > > which is wrong. If you wrap newChan in unsafePerformIO then the compiler > will feel free to apply rewrites like the above, which is unlikely to be > what you wanted. > > Nick > -----Original Message----- > From: haskell-bounces(a)haskell.org [mailto:haskell-bounces@haskell.org] > On Behalf Of S. Alexander Jacobson > Sent: 23 April 2004 19:22 > To: Haskell Mailing List > Subject: [Haskell] Why is newChan in the IO Monad? > > Nothing actually happens when newChan is called > except construction of a new datastructure. It > would be nice to have non IO monad code be able to > create a new Chan that gets passed to IO code that > uses it somewhere else. > > Alternatively, is there a way to create a Chan > outside the IO monad? > > -Alex- > > _________________________________________________________________ > S. Alexander Jacobson mailto:me@alexjacobson.com > tel:917-770-6565 http://alexjacobson.com > _______________________________________________ > Haskell mailing list > Haskell(a)haskell.org > http://www.haskell.org/mailman/listinfo/haskell >

1 0

AFP 2004 - Call for Participation
by afp04＠cs.ut.ee 23 Apr '04

23 Apr '04

[Early registration deadline: 14 May 2004.] Call for Participation AFP 2004 5th International Summer School on Advanced Functional Programming Tartu, Estonia 14-21 August 2004 http://www.cs.ut.ee/afp04 AFP is a series of international summer schools which aims to bring computer scientist, in particular young researchers and programmers, up to date with the latest advances in practical functional programming. The main focus of the school is on the interface between results presented at programming conferences and the programming in the real world. This is the fifth event in the series organized by the Department of Computer Science of the University of Tartu in conjuction with the Centre for Dependable Computing. The previous schools were held in Båstad (Sweden, 1995), Olympia (Washington, USA, 1996), Braga (Portugal, 1998) and Oxford (UK, 2002). PROGRAMME The scientific programme of AFP'04 consists of short courses by renowned experts of the field and a student session. The school offers eight main courses, each composed of lectures and accompanied by lab sessions. The course list is the following: John Hughes (Chalmers University of Technology): Arrows Conor McBride (University of Durham): Epigram: dependent types for practical programming Alberto Pardo (Universidad de la Republica, Montevideo): Combining datatypes and effects Rinus Plasmeijer (University of Nijmegen): Generic programming techniques for the construction of graphical user interfaces A strongly typed functional operating system based on dynamics Bernie Pope (University of Melbourne): Declarative debugging with Buddha Doaitse Swierstra (Utrecht University) and Atze Dijkstra (Utrecht University): Typing Haskell with an Attribute Grammar Peter Thiemann (University of Freiburg): Server-side Web programming in WASH Simon Thompson (University of Kent): Refactoring Functional Programs In addition, there will be some introductory and intermediate functional programming courses serving as a preparation for the advanced courses. The purpose of the student session is to give students an opportunity to present their work and get feedback. Everyone intending to give a presentation should submit an extended abstract (max 10 pp) along with the registration form. VENUE Tartu, with 100,000 inhabitants, is the second largest city in Estonia, situated 180 km south-east from Tallinn. Tartu University, founded 1632, is one of the oldest universities in Northern Europe. The school will be held in the new building of the Faculty of Mathematics and Computer Science. Tartu is accessible from Tallinn by coach. The coaches run very frequently (1-2 departures per hour) and the ride takes 2-2.5 hrs. Tallinn, with 400,000 inhabitants, is the capital city of Estonia, that used to be a member of the Hansa League. Tallinn's medieval Old Town is on the UNESCO World Heritage List. There are direct flights to Tallinn from London, Paris, Amsterdam, Frankfurt, Hamburg, Munich, Berlin, Prague, Warsaw, Moscow, Copenhagen, Oslo, Stockholm, Helsinki. IMPORTANT DATES May 14, 2004 Early registration deadline July 9, 2004 Late registration deadline REGISTRATION AND COST The registration is done through internet (http://www.cs.ut.ee/afp04/submreg.ht ml). The deadline for registration is July 9, 2004 and the registration fee is 330 EUR. For early registrants, until May 14, there is a reduced registration fee 280 EUR. The registration fee includes course materials distributed during the school, revised lecture notes published by Springer after the school, lunches, refreshments for coffee breaks and conference dinner. AFP'04 is an APPSEM II affiliated event, hence APPSEM II sites can use the project funds to support their students' participation in the school. PROGRAMME COMMITTEE / ORGANIZING COMMITTEE Varmo Vene University of Tartu Tarmo Uustalu Institute of Cybernetics Johan Jeuring Utrecht University SPONSORS Ministry of Education and Research (via the centres of excellence in research programme) APPSEM II - FP5 IST thematic network Applied Semantics II CONTACT afp04(a)cs.ut.ee

1 0

Why is newChan in the IO Monad?
by S. Alexander Jacobson 23 Apr '04

23 Apr '04

Nothing actually happens when newChan is called except construction of a new datastructure. It would be nice to have non IO monad code be able to create a new Chan that gets passed to IO code that uses it somewhere else. Alternatively, is there a way to create a Chan outside the IO monad? -Alex- _________________________________________________________________ S. Alexander Jacobson mailto:me@alexjacobson.com tel:917-770-6565 http://alexjacobson.com

2 1

ACL2 Workshop
by Matt Kaufmann 23 Apr '04

23 Apr '04

Greetings [and apologies if you get multiple copies]: The fifth ACL2 Workshop will be held November 18-19, 2004, in Austin Texas, USA, in conjunction with (and immediately following) FMCAD. We invite users of ACL2, users of other theorem provers, and persons interested in the applications of theorem proving technology to attend. ACL2 is a state-of-the-art automated reasoning system, which grew out of the Boyer-Moore theorem prover and has been used successfully on a number of industrial and academic projects. ACL2 is described at http://www.cs.utexas.edu/users/moore/acl2. The ACL2 workshops provide a forum for the presentation and discussion of projects using ACL2 as well as the evolution of the tool. Topics include the following. o applications of the theorem prover o improvements and extensions to the theorem prover o comparisons of ACL2 to other theorem provers, programming languages, or specification languages o solved challenge problems for ACL2 users (especially challenges that help newcomers learn the system) o implementations connecting ACL2 and other systems For more information, including a call for papers, see: http://www.cs.utexas.edu/users/moore/acl2/workshop-2004/ Relevant dates are as follows: Submission Deadline: July 26, 2004 Acceptance Notification: August 23, 2004 Registration without late fee: October 4, 2004 Workshop: November 18-19, 2004 Regards, Matt Kaufmann and J Moore (Organizing Committee)

1 0

evaluate function as a string
by Ay Joselito 23 Apr '04

23 Apr '04

Hello! I am new to Haskell. I want to develop an application in which the user enters a mathematical equation, presumably as a string (any arbitrary equation, using any of the standard mathematical operators : +,*,^, etc, and any of the standard functions: sin, exp, etc.). I need to take that string, convert it to a real function, and evaluate it. Thank you. ______________________________________________________________________ Correo Yahoo! - 6MB, más protección contra el spam ¡Gratis! http://correo.yahoo.es

4 4

Correct interpretation of the curry-howard isomorphism
by Bruno Oliveira 23 Apr '04

23 Apr '04

Hi all! I would like to know what is the right interpretation of one of the consequences of the curry-howard isomorphism. I know that there is a relation between being able to implement coerse :: a -> b, and the fact that a type system is sound. I thought this would be the right consequence: ------------------------------------------ if we can write a function: coerce :: a -> b then, this would mean (by the curry-howard isomorphism) that the type system is not sound. ------------------------------------------ but then, it would be too easy to write this in haskell: coerce :: a -> b coerce x = undefined As an obvious consequence, Haskell type system would be unsound. So, I assumed that this would be a wrong interpretation. Would the following be more correct? ------------------------------------------ if we can write a function: coerce :: a -> b without calling any other function or primitive (that is, just with making use of the type system), then this would mean that the type system is unsound. ------------------------------------------ I would appreciate if someone could provide me with the right interpretation. Thanks, in advance! Best Regards, Bruno Oliveira

3 2