Re: [Caml-list] elegant subtyping?
Thanks a lot everyone for all the tips and info -- it's working like a charm! Best regards -Markus On 4 Nov 2011, at 15:50, Vincent Aravantinos wrote: In the end, I think the choice of using polymorphic variants or not should not rely only on the types themselves but also mainly on the functions that you apply on them. More precisely: if there is no or very few common (simple) functions between Ast.statement and Cfg.statement functions, don't bother with polymorphic variants (you can still get rid of the copy pasting by defining your function only on one of the types, and then using translation to the other type to lift your function). On 11/04/2011 10:12 AM, Gabriel Scherer wrote: In theory, polymorphic variants are the right tool for the job : they allow to express exactly what is asked for -- even in presence of recursive datatypes, if carefully formulated using open recursion and fixpoint. See Jacques Garrigue paper Code reuse through polymorphic variants for an introduction and interesting examples : http://www.math.nagoya-u.ac.jp/~garrigue/papers/fose2000.html In practice, they come with the downside of being more difficult to use than closed variants. I personally keep using your solution (1) to preserve simplicity; that usually means a finite number of dumb-looking | Ast.Assign - Cfg.Assign branches in each pattern matching, but nothing really problematic for code quality or maintenance. The problem with polymorphic variants is that they are so flexible that type inference cannot help you a lot with errors in polymorphic variants code. For example, if you mistype one constructor name, the compiler won't be able to flag an error, it will only infer a slightly different types with the usual constructors, plus the misspelled one. Errors will only be spotted later, when you try to combine the faulty code with a function with strict assumptions on the variants (closed pattern matching), with an unwieldy error message. My advice for polymorphic variant beginners is to massively use annotations to control type-checking : every time you take a polymorphic variant as input, or output one, the function should be annotated with a precise type for the variant part. This will shield you from most inference issues, and force you to build an expressive set of type definitions (as Pietro demonstrated) that can be composed and help reason about your program. On Fri, Nov 4, 2011 at 2:43 PM, Pietro Abate pietro.ab...@pps.jussieu.fr wrote: hello, using polymorphic variants maybe ? # module Cfg = struct type statement = [ `Assign | `Guard ] end;; module Cfg : sig type statement = [ `Assign | `Guard ] end # module Ast = struct type statement = [ Cfg.statement | `Goto | `Label ] end;; module Ast : sig type statement = [ `Assign | `Goto | `Guard | `Label ] end p On Fri, Nov 04, 2011 at 02:06:23PM +0100, Markus Weißmann wrote: Hello everyone, I'm writing on a compiler and want to subtype the statements that can occur in my code: At first I have an abstract syntax tree that can hold any statement of the language. From that I create a control flow graph that will only have non-control-flow statements (a true subset of the Ast-statements). Whats the best way to realize that? Basically I have: module Ast: type statement = Assign | Guard | Goto | Label module Cfg: type statement = Assign | Guard I see three -- not so elegant -- solutions to this: 1.) type-safe but imho quite ugly code: module Cfg: type statement = Assign | Guard module Ast: type statement = Base of Cfg.statement | Goto | Label 2.) use the same type for both and give up the safety that wrong types cannot show up in the Cfg 3.) use objects Did I miss the type-safe, elegant, module-based solution somehow? Or is 1.) as good as it gets? Best regards -Markus -- Markus Weißmann, M.Sc. Institut für Informatik Technische Universität München Raum 03.07.054, Boltzmannstr. 3, 85748 Garching Tel. +49 (89) 2 89-1 81 05 Fax +49 (89) 2 89-1 81 07 mailto:markus.weissm...@in.tum.de -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs -- http://en.wikipedia.org/wiki/Posting_style -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs -- Vincent Aravantinos Postdoctoral Fellow, Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports:
RE: [Caml-list] How to write an efficient interpreter
If the language you are interpreting is quite declarative then piggy-backing on OCaml's run-time either by writing an interpreter or by compiling to OCaml code will be a big advantage. Writing a VM with a run-time as efficient as OCaml's in this context is a *lot* of work compared to writing an interpreter. Unless there is a compelling reason not to, I'd stick with an interpreter and just optimize it carefully. In particular, pay careful attention to your data representations. When writing a term-rewriter, one of the biggest performance gains I got was putting the value of each variable in the variable itself so it could be looked up by dereferencing a pointer rather than going via a hash table. Symbol tables are useful for similar reasons: map identifiers onto small integer IDs and replace hash tables that have identifiers as keys with an array indexed by ID. Beware the write barrier though. Also, when profiling I'd recommend logging the kinds of inputs your interpreter sees. For example, try to spot patterns in the shapes of expressions that your interpreter deals with and add special cases to the expression type for those shapes and custom code to interpret them. Cheers, Jon. -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] Call for Participation: APLAS+CPP
CALL FOR PARTICIPATION APLAS+CPP Kenting, Taiwan December 4 to 9, 2011 APLAS aims at stimulating programming language research by providing a forum for the presentation of latest results and the exchange of ideas in topics concerned with programming languages and systems. APLAS is based in Asia, but is an international forum that serves the worldwide programming language community. CPP is a new international forum on theoretical and practical topics in all areas, including computer science, mathematics, and education, that consider certification as an essential paradigm for their work. Certification here means formal, mechanized verification of some sort, preferably with production of independently checkable certificates. CPP targets any research promoting formal development of certified software and proofs. For the first time, APLAS and CPP will be held together in Kenting, Taiwan from December 4 to 9, 2011. The six-day event includes two tutorials, six invited talks, and two conferences. We offer a special rate for participants who register to both conferences. For the detailed program of each conference, please go to their respective web sites: http://flolac.iis.sinica.edu.tw/aplas11/doku.php (APLAS) http://formes.asia/cpp/ (CPP) Early Registration (until November 12, 2011) Regular | Student ---+--- APLAS+CPP: TWD 24000 | TWD 19500 APLAS only: TWD 16500 | TWD 13500 CPP only: TWD 16500 | TWD 13500 Location The conferences will be held in Kenting, a seaside resort and national park in Southern Taiwan. Temperatures in Kenting averaged at 21.4 C in December 2010 (high: 29.5, low: 14.3). It can be a bit windy, but the weather probably is the best in Taiwan in December. You can find more information about the Kenting National Park at Wikipedia and Wikitravel. The conference venue is Howard Beach Resort Kenting. Keynote Speakers o Andrew Appel (Princeton University) VeriSmall: Verified Smallfoot Shape Analysis o Nikolaj Bjorner (Microsoft Research) Engineering Theories with Z3 o Ranjit Jhala (UC San Diego) Software Verification with Liquid Types o Peter O'Hearn (Queen Mary, University of London) Algebra, Logic, Locality, Concurrency o Sriram Rajamani (Microsoft Research India) Program Analysis and Machine Learning: A Win-Win Deal o Vladimir Voevodsky (Institute for Advanced Study, Princeton) Univalent Semantics of Constructive Type Theories Tutorials o Lei Liu (Chinese Academy of Sciences) Parallelizing Legacy Sequential Code o Shin-Cheng Mu (Academia Sinica) Dependently Typed Programming in Adga Panels o Certificates (moderator: Dale Miller) o Teaching with Proof Assistants List of Accepted Papers APLAS o Thao Dang and Thomas Martin Gawlitza. Time Elapse over Template Polyhedra in Polynomial Time through Max-Strategy Iteration o David Monniaux and Martin Bodin. Modular Abstractions of Reactive Nodes using Disjunctive Invariants o Elvira Albert, Puri Arenas, Samir Genaim, Miguel Gomez-Zamalloa and German Puebla. Cost Analysis of Concurrent OO Programs o Benoit Boissinot, Florian Brandner, Alain Darte, Benoit Dupont De Dinechin and Fabrice Rastello. A Non-Iterative Data-Flow Algorithm for Computing Liveness Sets in Strict SSA Programs o Dmitriy Traytel, Stefan Berghofer and Tobias Nipkow. Extending Hindley-Milner Type Inference with Coercive Subtyping o Patrick Baillot. Elementary linear logic revisited for polynomial time and an exponential time hierarchy o Zhen Cao, Yuan Dong and Shengyuan Wang. Compiler Backend Generation for Application Specific Instruction Set Processors o Akimasa Morihata. Macro Tree Transformations of Linear Size Increase Achieve Cost-optimal Parallelism o Jade Alglave, Daniel Kroening, John Lugton, Vincent Nimal and Michael Tautschnig. Soundness of Data Flow Analyses for Weak Memory Models o Yulei Sui, Sen Ye, Jingling Xue and Pen-Chung Yew. SPAS: Scalable Path-Sensitive Pointer Analysis on Full-Sparse SSA o Keiko Nakata, Tarmo Uustalu and Marc Bezem. A Proof Pearl with the Fan Theorem and Bar Induction: Walking through Infinite Trees with Mixed Induction and Coinduction o Ulrich Schoepp. Computation-by-Interaction with Effects o Ashutosh Gupta, Corneliu Popeea and Andrey Rybalchenko. Solving Recursion-Free Horn Clauses over LI+UIF o Hakjoo Oh and Kwangkeun Yi. Access-based Localization with Bypassing o Yun-Yan Chi and Shin-Cheng Mu. Constructing List Homomorphisms from Proofs o Jonas Magazinius, Aslan Askarov and Andrei Sabelfeld. Decentralized Delimited Release o Filippo Bonchi, Fabio Gadducci and Giacoma Monreale. Towards A General Theory of Barbs, Contexts and Labels o Lukasz Fronc and Franck Pommereau. Towards a Certified Petri Net Model-Checker o Fernando Saenz-Perez. A Deductive Database with Datalog and SQL Query Languages o Yuichiro
