Syntax extension for Monads in Ocaml Jacques Carette, Lydia E. van Dijk and Oleg Kiselyov This Camlp4 extension provides some syntactic sugar to beautify monadic expressions. Example: A simple but realistic example of the use of a list monad looks like this bind [1; 2; 3] (fun a -> bind [3; 4; 5] (fun b -> return (a + b))) where we assume the appropriate definitions of the functions "bind" and "return". With the help of "pa_monad" this can be written as perform a <-- [1; 2; 3]; b <-- [3; 4; 5]; return (a + b) which is much clearer and thus easier to understand and maintain. By the way, the expression evaluates to [4; 5; 6; 5; 6; 7; 6; 7; 8] the sum of each pair of values of the input list
1. What is a dependent type 1. ADT -- the simplest dependent-type 2. Singleton types 3. Branding: type proxies 2. Lightweight static capabilities 1. Abstract and Introduction 2. Formalization and proofs 3. Accompanying source code 3. The question of verification 4. Genuine Dependent-type systems This is a joint work with Chung-chieh Shan. We describe several approaches to lightweight dependent-type programming, letting us gain experience with dependent types on existing programming language systems All these lightweight approaches rely on type-level proxies for values, so we can statically express properties (e.g., equality, inequality) of the values that are not generally known until the run time. ``This much is clear: many programmers are already finding practical uses for the approximants to dependent types which mainstream functional languages (especially Haskell) admit, by hook or by crook.''
This paper describes practical programming with types parameterized by numbers: e.g., an array type parameterized by the array's size or a modular group type Zn parameterized by the modulus. An attempt to add, for example, two integers of different moduli should result in a compile-time error with a clear error message. Number-parameterized types let the programmer capture more invariants through types and eliminate some run-time checks. Oleg shows several approaches towards encoding numbers into types and using those numbers to check list length, matching sizes for matrices or vectors. Oleg also points out connections to dependent types, phantom types, and shape-invariant programming.
demonstrates that sprintf and sscanf can indeed use exactly the same formatting specification, which is a first-class value. We demonstrate typed sprintf and typed sscanf sharing the same formatting specification. Our solution is surprisingly trivial: it defines a simple embedded domain-specific language of formatting patterns. The functions sprintf and sscanf are two interpreters of the language, to build or parse a string according to the given pattern. Our solution relies only on GADTs. We demonstrate that lambda-abstractions at the type level are expressible already in the Hindley-Milner type system; GADT with the included polymorphic recursion help us use the abstractions.
Interpreting types as abstract values [The Abstract of the lecture notes] We expound a view of type checking as evaluation with `abstract values'. Whereas dynamic semantics, evaluation, deals with (dynamic) values like 0, 1, etc., static semantics, type checking, deals with approximations like int. A type system is sound if it correctly approximates the dynamic behavior and predicts its outcome: if the static semantics predicts that a term has the type int, the dynamic evaluation of the term, if it terminates, will yield an integer. As object language, we use simply-typed and let-polymorphic lambda calculi with integers and integer operations as constants. We use Haskell as a metalanguage in which to write evaluators, type checkers, type reconstructors and inferencers for the object language.