- Haskell - Haskell.org

Injecting stateful computations into pure Haskell code.
by szefirov＠ot.ru 21 Sep '06

21 Sep '06

It is widely spread convention to simulate electronic circuits using infinite lazy lists. This works well for high level modeling, but when engineers ask to cosimulate it with Verilog or VHDL modules it goes somewhat off of pure functional programming. The main obstacle is that those modules have their own internal state. Is it possible to represent a result of several impure calculation as a pure list? The only way I can think of is the use of unsafePerformIO. Maybe State monad will help? And how?

2 1

ANNOUNCE: Codec.Compression.GZip & .BZip
by Duncan Coutts 21 Sep '06

21 Sep '06

I'm pleased to announce two new packages: zlib and bzlib which provide functions for compression and decompression in the gzip and bzip2 formats: Both provide pure functions on streams of data represented by lazy ByteStrings: compress, decompress :: ByteString -> ByteString This makes it easy to use either in memory or with disk or network IO. For example a simple gzip compression program is just: > import qualified Data.ByteString.Lazy as ByteString > import qualified Codec.Compression.GZip as GZip > > main = ByteString.interact GZip.compress Or you could lazily read in and decompress @.gz@ file using: > content <- fmap GZip.decompress (readFile file) The code is available via darcs: darcs get http://haskell.org/~duncan/zlib darcs get http://haskell.org/~duncan/bzlib (Note that if you are using GHC-6.5 then you'll need to edit the .cabal file to remove the dependency on fps, since ByteStrings are provided in the base package in GHC-6.5.) There is API documentation too: http://haskell.org/~duncan/zlib/docs http://haskell.org/~duncan/bzlib/docs Both packages are bindings to the corresponding C libs, so they depend on those C libraries. Fortunately both zlib and bzlib2 are available on every OS. It also means that the compression speed is as you would expect since it's the C lib that is doing all the work. I'm very happy to get feedback on the API, the documentation or of course any bug reports. Duncan

2 1

Deferred instance declarations (serialization of existential boxes)
by Misha Aizatulin 21 Sep '06

21 Sep '06

hello all, I asked this question on haskell-cafe once, but my post didn't get any responses, so I try once again here explaining a bit more where my problem comes from. Suppose I have a monomorphic datatype, say T and want to do something with it, which depends on an instance of class C being defined for T. However I can only provide this instance later, in a different module. So I would like to write something like > f :: C T => T -> T or > instance C T => C T' where > -- a body that uses functions from C T By this I mean that f can only be called or C T' can only be derived in a module that defines C T. However, I don't see any way to make this work with ghc. Note that if I had a polymorphic type like (T a), everything would be fine. What I need it for is serialization of datatypes with existential constructors (see http://haskell.org/pipermail/haskell-cafe/2006-September/018041.html) I am having a box like > data Box = forall a. Cxt a => Box a and want to write a Read instances for it. The problem is that currently I can only do that when I am aware of all types that will ever go into the box, which is not in the same module where the Box is defined. But there is code in the same module that needs to refer to this instance. I hope you see now where my problem comes from. I would be very thankful for any help or suggestions. If someone has implemented serialization with existentials before, it would be really interesting, if they had a similar problem. Another question: would it be possible to allow definitions of f and C T' above in GHC? Cheers, Misha P.S. Currently I am solving this problem by introducing recursively dependent modules.

3 2

Haskell Weekly News: September 18, 2006
by dons＠cse.unsw.edu.au 20 Sep '06

20 Sep '06

--------------------------------------------------------------------------- Haskell Weekly News http://haskell.org/haskellwiki/HWN Issue 41 - September 18, 2006 --------------------------------------------------------------------------- Welcome to issue 41 of HWN, a weekly newsletter covering developments in the Haskell community. Each week, new editions are posted to [1]the Haskell mailing list as well as to [2]the Haskell Sequence and [3]Planet Haskell. [4]RSS is also available, and headlines appear on [5]haskell.org. The 2006 Haskell Workshop was held today in Portland, Oregon. Thanks to Edward Kmett for a report on the event. 1. http://www.haskell.org/mailman/listinfo/haskell 2. http://sequence.complete.org/ 3. http://planet.haskell.org/ 4. http://sequence.complete.org/node/feed 5. http://haskell.org/ Announcements * Haskell98 Termination Analyser . Stephan Swidersk [6]announced the integration of an automatic Haskell98 termination analyzer in the termination tool AProVE. The tool accepts full Haskell as specified in the Haskell 98 Report and is available through our web interface. [7]More 6. http://article.gmane.org/gmane.comp.lang.haskell.general/14193 7. http://aprove.informatik.rwth-aachen.de/ * Free theorems . Janis Voigtlaender [8]announced that Sascha Boehme has done a project to implement the Reynolds/Wadler algorithm generating theorems from polymorphic types, plus simplifications and postprocessings for such free theorems. [9]More info 8. http://article.gmane.org/gmane.comp.lang.haskell.general/14160 9. http://haskell.as9x.info/ * Haddock/GHC SoC . David Waern [10]announced a short status report of the "Port Haddock to use GHC" Summer of Code project. The GHC modifications, are finished and will be included in the GHC head repository soon. 10. http://article.gmane.org/gmane.comp.lang.haskell.general/14149 * AutoForms release 0.2 . Mads Lindstr�m [11]released AutoForms 0.2, a library to ease the creation of GUIs. It does this by using generic programming (SYB) to construct GUI components. [12]More info 11. http://article.gmane.org/gmane.comp.lang.haskell.general/14148 12. http://autoforms.sourceforge.net/ * HSPClientside 0.2 . Joel Bj�rnson [13]announced a new version of HSPClientside (0.2) ,developed as a GSoC project during this summer. HSPClientside is a Haskell Server Pages library for generating JavaScript code. [14]More info 13. http://article.gmane.org/gmane.comp.lang.haskell.general/14133 14. http://darcs.haskell.org/SoC/hsp.clientside/ * SOE implementation based on Gtk2Hs . Duncan Coutts [15]Due to popular demand the new SOE implementation based on Gtk2Hs is [16]available. The rendering quality is better than the original HGL version. [17]Here's a side-by-side comparison 15. http://article.gmane.org/gmane.comp.lang.haskell.general/14132 16. file://localhost/home/dons/dons/src/hwn/now 17. http://haskell.org/~duncan/gtk2hs/SOE-cairo.png * The experimental GHCi debugger . Pepe [18]announced the results of his SoC project, the experimental Haskell debugger. [19]More details 18. http://article.gmane.org/gmane.comp.lang.haskell.general/14131 19. http://haskell.org/haskellwiki/GHC/GHCiDebugger * SmallCheck . Colin Runciman [20]released a prototype tool that is similar in spirit, and in some of its workings, to QuickCheck. SmallCheck is, though, based on exhaustive testing in a bounded space of test values. [21]More info 20. http://article.gmane.org/gmane.comp.lang.haskell.general/14129 21. http://www.cs.york.ac.uk/fp/smallcheck0.0.tar * Frisby: composable, linear time parser for arbitrary PEG grammers . John Meacham [22]released Frisby, an implementation of the 'packrat' parsing algorithm, which parse PEG grammars and have a number of very useful qualities, they are a generalization of regexes in a sense that can parse everything in LL(k), LR(k), and more, including things that require unlimited lookahead, all in guaranteed linear time. [23]More information 22. http://article.gmane.org/gmane.comp.lang.haskell.general/14128 23. http://repetae.net/computer/frisby/ * HaskellNet . Jun Mukai [24]published a status report on the state of his SoC project, HaskellNet 24. http://article.gmane.org/gmane.comp.lang.haskell.general/14126 * GHC's new support engineer . Simon Marlow [25]announced that GHC now has a full-time support engineer, Ian Lynagh (aka Igloo on IRC). He'll be helping with all aspects of GHC, especially release management, bug diagnosis and tracking, documentation, packaging, and supporting other GHC hackers. Welcome Ian! 25. http://article.gmane.org/gmane.comp.lang.haskell.general/14125 Haskell' This section covers the [26]Haskell' standardisation process. * [27]Writing / status teams - call for volunteers * [28]do and if then else * [29]map and fmap * [30]All monads are functors 26. http://hackage.haskell.org/trac/haskell-prime 27. http://article.gmane.org/gmane.comp.lang.haskell.prime/1657 28. http://article.gmane.org/gmane.comp.lang.haskell.prime/1599 29. http://thread.gmane.org/gmane.comp.lang.haskell.prime/1625/focus=1625 30. http://thread.gmane.org/gmane.comp.lang.haskell.prime/1590/focus=1590 Discussion The Haskell Workshop . Here is a summary of the talks presented today at the Haskell Workshop * RepLib: A Library for Derivable Type Classes . Stephanie Weirich [31]presented a neat library for generic traversals. It covered just about everything you'd need and seemed pretty painless to use. From the abstract: Some type class instances can be automatically derived from the structure of types. As a result, the Haskell language includes the "deriving" mechanism to automatic generates such instances for a small number of built-in type classes. In this paper, we present RepLib, a GHC library that enables a similar mechanism for arbitrary type classes. 31. http://www.cis.upenn.edu/~sweirich/RepLib/ * A Generic Recursion Toolbox for Haskell (Or: Scrap Your Boilerplate Systematically) . Deling Ren and Martin Erwig [32]talked about another generics library, with a neat core "mother traversal" that abstracted over different data structure traversals. The Recursion Library for Haskell provides a rich set of generic traversal strategies to facilitate the flexible specification of generic term traversals. The underlying mechanism is the Scrap Your Boilerplate (SYB) approach. Most of the strategies that are used to implement recursion operators are taken from Stratego. 32. http://web.engr.oregonstate.edu/~erwig/reclib/ * Strong Types for Relational Databases . Alexandra Silva and Joost Visser [33]presented a relational database Using the type system to encode not only the types of fields it was joining, but a bit more about their meaning and role in the key. Type-level programming is used to maintain the consistency between header and rows, and between functional dependencies and tables. Type-level predicates are provided to check whether tables and functional dependencies are in particular normal-forms, or not. 33. http://lmf.di.uminho.pt/wiki/pub/PURe/CoddFish/StrongTypesForRDBs-draft-04-… * Polymorphic Variants in Haskell . Koji Kagawa [34]presented a paper on polymorphic variants in Haskell, describing some interesting type system extensions. In languages that support polymorphic variants, a single variant value can be passed to many contexts that accept different sets of constructors. Polymorphic variants are potentially useful for application domains such as interpreters, graphical user interface (GUI) libraries and database interfaces, where the number of necessary constructors cannot be determined in advance. 34. http://guppy.eng.kagawa-u.ac.jp/~kagawa/PVH * Extended Static Checking for Haskell . Dana Xu [35]gave a great talk on ESC/Haskell, proving the partial correctness of programs with compile time checks for pre/postcondition violations, and using an external theorem prover to prove bits about arithmetic expressions. Very practical stuff. The extended static checking is beautiful in that it opens up a whole new arena in Haskell for machine checkable documentation. 35. http://www.cl.cam.ac.uk/~nx200/ * Running the Manual: An Approach to High-Assurance Microkernel Development . Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock and Manuel M.T. Chakravarty [36]presented a microkernel paper. This was really good. Before I saw the talk I really questioned the judgement of prototyping a microkernel in Haskell. Now I want to go prototype one myself. We propose a development methodology for designing and prototyping high assurance microkernels, and describe our application of it. The methodology is based on rapid prototyping and iterative refinement of the microkernel in a functional programming language. 36. http://www.cse.unsw.edu.au/~chak/papers/DEKC+06.html * Strongly Typed Memory Areas -- Programming Systems-Level Data Structures in a Functional Language . Iavor S. Diatchki and Mark P. Jones [37]gave a presentation on how you could extend the type system to include an extra kind for physical memory regions and data representations in memory, with endianness, and the like. He implemented it in a kind of strict pseudo-Haskell, but the general notation was pretty clean and would be usable for system level programming in Haskell. 37. http://www.cse.ogi.edu/~diatchki/papers/haskell007-diatchki.pdf * User-Level Transactional Programming in Haskell . Peter Thiemann wrote on generalizing the interface for STM to other kinds of database and user-interface transactions, where he gave up the ability to automatically retry blocking on a changeset of TVars, producing a kind of transaction that could actually fail and be manually retried. * An Extensible Dynamically-Typed Hierarchy of Exceptions . Simon Marlow [38]presented an extensible exception hierarchy using type classes. In this paper we address the lack of extensibility of the exception type in Haskell. We propose a lightweight solution involving the use of existential types and the Typeable class only, and show how our solution allows a fully extensible hierarchy of exception types to be declared, in which a single overloaded catch operator can be used to catch either specific exception types, or exceptions belonging to any subclass in the hierarchy. 38. http://www.haskell.org/~simonmar/papers/ext-exceptions.pdf * Demo: Introducing the Haskell Equational Reasoning Assistant . Andy Gill came in and did a really neat, high energy, demo of an interactive equational reasoning/code refactoring tool. He actually loaded up the application and showed it refactoring live. * GenI: Natural Language Generation in Haskell . Eric Kow [39]covered genI and gave a user's level overview of the features in Haskell that are useful in real code. The natural language generation stuff there was pretty nifty. 39. http://hal.inria.fr/docs/00/08/87/87/PDF/haskell01-kow.pdf * Demo: Typed Linear Algebra . Frederik Eaton covered a linear algebra library with ATLAS and LAPACK bindings in Haskell that uses type level enumerable values to provide its bounds. Neat stuff. * Demo: Interactive Debugging . David Himmelstrup unforutnately was unable to present [40]his talk, due to illness. From the abstract: Haskell's lazy nature is a large part of its beauty. Unfortunately, laziness complicates debugging in the "stop, examine, continue" sense, and hence tools such as Freja, Hat and Hood have risen. This paper describes the implementation of a "stop, examine, continue" debugger for Glasgow Haskell 40. http://darcs.haskell.org/~lemmih/hw2006.ps * Demo: The Galois Haskell Program Coverage tool, HPC . A demo was presented on how you can use HPC to interactively control QuickCheck, get it to run some cases, and check to see how much coverage you have had, then have it run more cases if thats not enough. The notion of looking at the difference in the coverage sets between a good run and a bad run to try to isolate bugs seems really useful. * Demo: On computable types . Oleg Kiselyov [41]presented a "proof by example" that the Haskell type system is Turing complete, with a 5 line type system lambda calculus and a 6 line type level fibonacci. 41. http://www.haskell.org/pipermail/haskell/2006-September/018486.html * Haskell' Status Report -- An Update on the Next Haskell Standard . Isaac Jones Isaac gave a talk on the state of [42]Haskell' 42. http://hackage.haskell.org/trac/haskell-prime Quotes of the Week * Baughn : "I think I'm beginning to understand this language. I just defined: let 1 + 1 = 3" * SamB : "Haskell is the only language I know with first-class support for imperative programming" * David Amos : "The real reason for using Haskell is that the code comes out shorter, and is quicker to write, than in imperative languages .. What that means is, I can get much more done when I use Haskell" * SyntaxNinja : "I recommend seeing if people have a major problem, then pouring concrete on them, and implementing what you want anyway" * SamB : "I was just saying that encasing poeple in concrete is not the best solution to that problem" * Sean Russell : "[On the wmii window manager mailing list] Hah! That's a laugh. Since when does 'it compiles' equate to 'it will run (correctly)'? We're talking about C, after all... not Haskell." * Adaptec : "[In documentation for one of their chipsets] We have a disclaimer because there may be corner cases" * audreyt : "Yes, I'm aware that I'm abusing GHC beyond its designed purpose" * cjeris : "I have a little perl script that aliases gcc -freduced-suckage to ghc" * dibblego : "Using logic in imperative programming language channels is generally considered trolling" * edwardk : "lambdabot is the first irc bot I ever added to my buddy list" * gmh33 : "Haskell makes so much more sense now and all I did was figure out the typing thing" * musasabi : "reallyUnsafePointerEq# seems unsafe" * sieni : "The advantage of Haskell is that it doesn't suck" * therp : "Good morning. I think I have been dreaming of shift/reset continuations" Contributing to HWN To help create new editions of this newsletter, please see the [43]contributing information. Send stories to dons at cse.unsw.edu.au. The darcs repository is available at darcs get http://www.cse.unsw.edu.au/~dons/code/hwn 43. http://haskell.org/haskellwiki/HWN

3 2

PLAN-X 2007: Call for Papers and Demos (Deadline Extended)
by Torsten Grust 20 Sep '06

20 Sep '06

Third Call for Papers and Software Demonstrations P L A N - X 2 0 0 7 Programming Language Techniques for XML An ACM SIGPLAN Workshop colocated with POPL 2007 Nice, France -- January 20, 2007 http://www.plan-x-2007.org/ || The submission deadline for PLAN-X 2007 has been || || postponed by a few days. New submission deadline: || || Tuesday, October 10, 2006, 5 PM (PDT) || -- PLAN-X 2007 Aim and Scope The XML data model and its associated languages add interesting twists to programming language practice as well as theory. Just like its four predecessors, the PLAN-X 2007 workshop turns the spotlight on how programming languages can embrace, for example, tree-shaped XML data structures, regular expression types extracted from schema descriptions, very small or large XML instances, queries against XML data, and XML transformations. XML reaches deep into all aspects of language design, type systems, compilers, as well as runtimes and PLAN-X 2007 is THE forum to present and discuss novel research work in this area. We invite contributions -- papers as well as software demonstrations -- from members of the programming language, database, theory, and document processing communities and look forward to a workshop in which this diversity of contributions and attendees leads to lively discussion and a fun event. If you are architecting a software system that fuses programming language and XML technology in interesting and innovative ways, please submit a software demonstration proposal to PLAN-X 2007. The workshop program will feature a special demo session. A two-page description of the accepted software demonstrations will be included in the proceedings. PLAN-X 2007 will be held in cooperation with and just after POPL 2007, the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages in the Plaza Hotel in Nice, France, on Januar 20, 2007. -- PLAN-X 2007 Topics of Interest Topics of interest include the following (though interesting and/or innovative papers on all aspects of programming languages for XML are welcome): - Design of programming and query languages for XML - Programming in the XML data model itself (e.g., extending XQuery into a full-fledged programming language) - Formal accounts of XML and its processors (based on logic, automata, variants of lambda calculus, etc.) - Compilers and interpreters for XML-aware languages and optimization techniques - Type systems, schema languages, and other constraints (e.g., keys) for tree-shaped data - Tree automata and transducers - Languages and systems that can cope with XML fragments (messages) or very large XML instances (beyond main-memory size) - Programming language glue between browsers, web services, and databases - Pioneering applications of XML-aware language technology -- Proceedings Accepted submissions will be collected to form the informal PLAN-X 2007 proceedings, to be indexed on Michael Ley's DBLP site and distributed at the workshop. The material may thus be published elsewhere at a later date. -- Paper Format and Submission The web-based paper submission site for PLAN-X 2007 is open! Submit at URL http://www.easychair.org/PLANX2007/ (Please register as a New User to obtain a login and password for the submission site.) PLAN-X 2007 calls for contributions relevant to the open list of topics sketched above. We explicitly welcome reports on innovative, off-beat, and ''early stage'' approaches as long as the submission reports on original work not published or submitted elsewhere. - Please format your papers according to the ACM guidelines and SIG proceedings templates available at http://www.acm.org/sigs/pubs/proceed/template.html The mandatory submission file format is PDF. - Regular papers should not exceed 10 pages in length including references and appendices, but shorter abstracts (of, e.g., 2000 words) often suffice and are acceptable as well. - Software demonstration proposals are limited to 2 pages and should include a sketch of the methods you employ as well as a description of what exactly will be demoed. Please submit your demonstration proposal via the regular paper submission site and add "(Demo)" to your submission's title. -- Important Dates - Paper submission (extended): Tue, Oct 10, 2006, 5 PM (PDT) - Notification of acceptance: Sat, Nov 25, 2006 - Camera-ready copy due: Sun, Dec 17, 2006 - Workshop: Sat, Jan 20, 2007 -- PLAN-X 2007 Program Committee - Michael Benedikt (Lucent, USA) - Daniela Florescu (Oracle, USA) - Alain Frisch (INRIA Roquencourt, France) - Giorgio Ghelli, Chair (U Pisa, Italy) - Haruo Hosoya (U Tokyo, Japan) - Anders Møller (U Aarhus, Denmark) - Mukund Raghavachari (IBM T.J. Watson Research Center, USA) - Alan Schmitt (INRIA Rhône-Alpes, France) - Sophie Tison (U Lille, France) - Philip Wadler (U Edinburgh, UK) -- PLAN-X 2007 Workshop Chairs - General Chair - Program Chair Torsten Grust Giorgio Ghelli TU München U Pisa Munich, Germany Pisa, Italy grust(a)in.tum.de ghelli(a)di.unipi.it

1 0

Re: [Haskell] How to define Y combinator in Haskell
by David House 15 Sep '06

15 Sep '06

On 15/09/06, Haihua Lin <HaihuaLin(a)163.com> wrote: > Is there a way to define it in Haskell? Note that the function 'fix' (find the fixpoint of a function) already exists in Haskell, and is equivalent to the Y combinator. It's interesting that most (all?) fixed-point combinators don't typecheck. The Y combinator, and by extension recursion in general, has to be added as a constant to the language. -- -David House, dmhouse(a)gmail.com

3 3

Is there an example how to pass a string to VBA?
by Andreas Marth 15 Sep '06

15 Sep '06

Hallo everybody! I'm trying to pass a String to VBA and am totally stuck. Does anyody have a working example how to do this? I am interested in either a plain low level DLL or a COM DLL or anything else if there is something else. I hope someone did this already and can give me a helping hand. A nice weekend for everybody, Andreas

2 2

How to define Y combinator in Haskell
by Haihua Lin 15 Sep '06

15 Sep '06

Hi, Writing yc = \f -> (\x -> f(x x)) (\x -> f(x x)) causes type error. Is there a way to define it in Haskell? Thanks, Haihua

2 1

ETAPS 2007 - Call for Submissions
by João Saraiva 15 Sep '06

15 Sep '06

***************************************************************** *** *** *** ETAPS 2007 *** *** March 24 - April 1, 2007 *** *** Braga, Portugal *** *** *** *** http://www.di.uminho.pt/etaps07/ *** *** *** *** CALL FOR SUBMISSIONS *** *** *** *** Abstract submission deadline: 6th October, 2006 *** *** Full submission deadline: 13th October, 2006 *** *** *** ***************************************************************** The European Joint Conferences on Theory and Practice of Software (ETAPS) is the primary European forum for academic and industrial researchers working on topics related to Software Science. It is a confederation of five main conferences, several satellite workshops and other events. * Main Conferences - Call for Submissions: CC 2007 International Conference on Compiler Construction ESOP 2007 European Symposium on Programming FASE 2007 Fundamental Approaches to Software Engineering FOSSACS 2007 Foundations of Software Science and Computation Structures TACAS 2007 Tools and Algorithms for the Construction and Analysis of Systems See: http://www.di.uminho.pt/etaps07/conf.html * Workshops - Call for Submissions: For the complete list of workshops and their deadlines See: http://www.di.uminho.pt/etaps07/workshops.html * Tutorials - Call for Submissions: See: http://www.di.uminho.pt/etaps07/tutorials.html

1 0

On computable types. II. Flipping the arrow
by oleg＠pobox.com 14 Sep '06

14 Sep '06

Part I of the series introduced the type-level functional language with the notation that resembles lambda-calculus with case distinction, fixpoint recursion, etc. Modulo a bit of syntactic tart, the language of the type functions even looks almost like the pure Haskell. In this message, we show the applications of computable types, to ascribe signatures to terms and to drive the selection of overloaded functions. We can compute the type of a tree of the depth fib(N) or a complex XML type, and instantiate the read function to read the trees of only that shape. A telling example of the power of the approach is the ability to use not only (a->) but also (->a) as an unary type function. The former is just (->) a. The latter is considered impossible. In our approach, (->a) is written almost literally as (flip (->) a) This series of messages has been inspired by Luca Cardelli's 1988 manuscript ``Phase Distinctions in Type Theory'' http://lucacardelli.name/Papers/PhaseDistinctions.pdf and by Simon Peyton Jones and Erik Meijer's ``Henk: A Typed Intermediate Language'' http://www.research.microsoft.com/~simonpj/Papers/henk.ps.gz which expounds many of the same notions in an excellent tutorial style and in modern terminology. I'm very grateful to Chung-chieh Shan for pointing out these papers to me and for thought-provoking discussions. > {-# OPTIONS -fglasgow-exts #-} > {-# OPTIONS -fallow-undecidable-instances #-} > > module TypeFN where > import TypeLC -- Load part I of this series (prev message) Our first example comes from Cardelli's paper: defining the type Prop(n), of n-ary propositions. That is, Prop(2) should be the type Bool -> Bool -> Bool Prop(3) is the type of functions Bool -> Bool -> Bool -> Bool etc. Cardelli's paper (p. 10) writes this type as let Prop:: AllKK(N:: NatK) Type = recK(F:: AllKK(N:: NatK) Type) funKK(N:: NatK) caseK N of 0K => Bool; succK(M) => Bool -> F(M); let and2: Prop(2K) = fun(a: Bool) fun(b: Bool) a & b; Here 0K and 2K are type-level numerals of the kind NatK; recK is the type-level fix-point combinator. The computed type Prop(2) then gives the type to the term and2. In our system, this example looks as follows: > data Prop' > instance A (F Prop') f (F (Prop',f)) > instance A (F (Prop',f)) Zero Bool > instance E (f :< m) r => A (F (Prop',f)) (Su m) (Bool -> r) > type Prop = Rec (F Prop') > type Prop2 = E (F Prop :< N2) r => r > and2 = (\x y -> x && y) `asTypeOf` (undefined:: Prop2) We can compute types by applying type functions, just as we can compute values by applying regular functions. Indeed, let us define a StrangeProp of the kind NAT -> Type. StrangeProp(n) is the type of propositions of arity m, where m is fib(n). We compose together the already defined type function Prop2 and the type function Fib in the previous message. > data StrangeProp > instance E (F Prop :< (F Fib :< n)) r => A (F StrangeProp) n r > oddand4t :: E (F StrangeProp :< (F FSum :< N2 :< N2)) r => r > oddand4t = undefined > oddand5 = (\x1 x2 x3 x4 -> ((x1 && x2 && x3) &&) . and2 x4) > `asTypeOf` oddand4t *DepType> :t oddand4t oddand4t :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool We can do better, with the help of higher-order type functions. First we declare a few standard Haskell type constants as constants in our calculus, with trivial evaluation rules > instance E Bool Bool > instance E Int Int > instance E String String > instance E (a->b) (a->b) -- We could just as well evaluate under > instance E (a,b) (a,b) -- these We introduce the combinator Ntimes: |NTimes f x n| applies f to x n times. This is a sort of fold over numerals. > data Ntimes > instance A (F Ntimes) f (F (Ntimes,f)) > instance A (F (Ntimes,f)) x (F (Ntimes,f,x)) > instance A (F (Ntimes,f,x)) Zero x > instance E (F Ntimes :< f :< (f :< x) :< n) r => A (F (Ntimes,f,x)) (Su n) r > data ATC1 c > instance A (F (ATC1 c)) x (c x) We can then write the type of n-ary propositions Prop(N) in a different way, as an N-times application of the type constructor (Bool->) to Bool. > type PropN' n = E(F Ntimes :< (F (ATC1 ((->) Bool))) :< Bool :< n) r => r > and2' = (\x y -> x && y) `asTypeOf` (undefined:: PropN' N2) To generalize, > data ATC2 (c :: * -> * -> *) > instance A (F (ATC2 c)) x (F (ATC1 (c x))) -- currying of type constructors > type SPropN' n = E(F Ntimes :< (F (ATC2 (->)) :< Bool) :< Bool > :< (F Fib :< n)) r => r > test_spn4 = undefined::SPropN' (Su N3) *TypeFN> :t test_spn4 test_spn4 :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool The comparison of ATC1 with ATC2 shows two different ways of defining abstractions: as (F x) terms (`lambda-terms' in our calculus) and as polymorphic types (Haskell type abstractions). The two ways are profoundly related. The more verbose type application notation, via (:<), has its benefits. After we introduce another higher-order function > data Flip > instance A (F Flip) f (F (Flip,f)) > instance A (F (Flip,f)) x (F (Flip,f,x)) > instance E (f :< y :< x) r => A (F (Flip,f,x)) y r we make a very little change > type SSPropN' n = E(F Ntimes :< (F Flip :< (F (ATC2 (->))) :< Bool) :< Bool > :< (F Fib :< n)) r => r > test_sspn4 = undefined::SSPropN' (Su N3) and obtain quite a different result: *TypeFN> :t test_sspn4 test_sspn4 :: ((((Bool -> Bool) -> Bool) -> Bool) -> Bool) -> Bool In effect, we were able to use not only (a->) but also (->a) as an unary type function. Moreover, we achieved the latter by almost literally applying the flip function to the arrow type constructor (->). Using the type inspection tools (typecast), we can replace the family of functions ATC1, ATC2 with one, kind-polymorphic, polyvariadic function ATC. This approach will be explained in further messages. We can use the computed types to drive overloaded functions such as read and show. The specifically instantiated read functions, in particular, will check that a (remotely) received serialized value matches our expectation. Let's consider the type of trees of the depth of at most N. > data Node v els = Node v [els] deriving (Read, Show) > type TreeDN v l n = E(F Ntimes :< (F (ATC1 (Node v))) :< l :< n) r => r > instance E (Node v els) (Node v els) > read_tree3 s = (read s) `asTypeOf` (undefined:: TreeDN Int String N3) *TypeFN> :t read_tree3 read_tree3 :: String -> Node Int (Node Int (Node Int String)) > ttree3_1 = read_tree3 "Node 1 [Node 2 []]" > ttree3_2 = read_tree3 "Node 1 [Node 2 [Node 3 [\"ok\"]]]" > ttree3_3 = read_tree3 "Node 0 [Node 1 [Node 2 [Node 3 [\"ok\"]]]]" *TypeFN> ttree3_2 Node 1 [Node 2 [Node 3 ["ok"]]] *TypeFN> ttree3_3 *** Exception: Prelude.read: no parse The ability of computed types to drive the selection of overloaded functions has wider implications. We can remove the need for functional dependencies, or simulate functional dependencies when they cannot apply. For example, one may define a multi-parameter typeclass but cannot assert functional dependencies, because not all instances satisfy them. Therefore, using the methods of the class may require complex and annoying type annotations. Computed types remove the need to manually write these annotations; the typechecker can compute them itself. This subject is to be explored further. The last example showed computations of polymorphic types, which, unsurprisingly, have the form of type abstractions. Our calculus is built around the deep connection between type abstraction/instantiation and functional abstraction/application.

1 0