From 4486370c94a78f4ea782d9c8b4d0a52d6c2d3396 Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Mon, 16 Dec 2019 03:39:46 +0200 Subject: [PATCH] README.txt -> README.md --- .prettierrc | 7 + README.md | 384 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 391 insertions(+) create mode 100644 .prettierrc create mode 100644 README.md diff --git a/.prettierrc b/.prettierrc new file mode 100644 index 00000000..3030ecd3 --- /dev/null +++ b/.prettierrc @@ -0,0 +1,7 @@ +{ + "bracketSpacing": false, + "printWidth": 80, + "semi": false, + "singleQuote": true, + "proseWrap": "always" +} diff --git a/README.md b/README.md new file mode 100644 index 00000000..eb6bee63 --- /dev/null +++ b/README.md @@ -0,0 +1,384 @@ +# 1ML TOY INTERPRETER [![Gitter](https://badges.gitter.im/1ml-prime/community.svg)](https://gitter.im/1ml-prime/community) [![Build Status](https://travis-ci.org/1ml-prime/1ml.svg?branch=1ml-prime)](https://travis-ci.org/1ml-prime/1ml) + +(c) 2014 Andreas Rossberg + +## Introduction + +This provides a simple proof-of-concept interpreter for a small version of 1ML, +an ML dialect based on first-class modules, as described in the paper + +
+
1ML - core and modules as one (F-ing first-class modules)
+
(submitted to ICFP 2015)
+
+ +The interpreter has been written mainly for the purpose of experimenting with +1ML type checking. + +A few caveats to keep in mind: + +- There are some minor differences to the language described in the paper. + +- The language is very basic, and misses lots of features you would expect from + a real ML, especially datatypes. + +- Error messages are rather basic, and types are always output in internal F-ing + notation, with no attempt to abbreviate. + +- It is slow and probably buggy. In particular, type checking is implemented + very naively, as a direct transliteration of the rules, with no worries about + efficiency. Type inference is best considered work in progress. :) + +- There is no documentation other than this file, and no sample code to speak + of. See [prelude.1ml](prelude.1ml) for some simple library code, and + [paper.1ml](paper.1ml) for the examples from the paper. + +Nevertheless, feedback on bugs or other comments are highly welcome +(). + +### Building + +You need OCaml 4.02 (or higher) and Make to build 1ML. Then just invoke: + +```bash +make +``` + +This creates an executable `1ml` in the source directory. + +### Running + +The synopsis for running the interpreter is: + +```bash +1ml [option] [file ...] +``` + +It evaluates the 1ML source files in the order they are given. If no file names +are provided, or one of the arguments is `-`, you will enter an interactive +prompt, in which can evaluate 1ML definitions (bindings, not expressions!) +directly. + +In order to have some basic types pre-defined, invoke the interpreter with the +prelude: + +```bash +1ml prelude.1ml - # interactive +1ml prelude.1ml myfile.1ml # batch +``` + +There are a number of command line options, which can be displayed with `-help`. +Most of them are only for internal debugging purposes. + +## The Language + +In 1ML, the traditional distinction between ML core and module layer has been +completely eliminated. Every expression conceptually is a "module". + +### Kernel Syntax + +The BNF below gives the kernel syntax for 1ML. Additional syntax is defined as +derived in the next section. A program consists of a sequence of bindings. + +``` + (types) + T ::= + E (projection from a value/module) + type (the type/kind of small types) + { D } (record/structure type) + (X : T) -> E (impure function/functor/constructor type) + (X : T) => E (pure function/functor/constructor type) + '(X : T) => E (implicit function/functor/constructor type) + (= E) (singleton/alias type) + T with .Xs = E (type refinement) + wrap T (impredicative wrapped type) + _ (type wildcard) + T as T (layered type (both operands have to be equal)) + + (declarations) + D ::= + X : T (field/member declaration) + include T (type/signature inclusion) + D ; D (sequencing) + (empty) + + (expressions) + E ::= + X (variable) + 123 (integer literal) + 'c' (character literal) + "text" (text literal) + type T (type value) + { B } (record/structure) + E.X (projection) + fun (X : T) => E (function/functor/constructor) + fun ‘(X : T) => E (implicit function/functor/constructor) + E E (application) + if E then E else E : T (conditional) + wrap E : T (impredicative wrapping) + unwrap E : T (unwrapping) + rec (X : T) => E (recursion) + @T E (recursive type roll) + E.@T (recursive type unroll) + + (bindings) + B ::= + X = E (field/member definition) + include E (record/structure inclusion) + B ; B (sequencing) + (empty) +``` + +Comments are written in one of the following form: + +``` + (; ... ;) + ;; ... (extends to end of line) + ;;;; ... (extends to end of file) +``` + +### Extended Syntax + +A number of derived forms (syntactic sugar) are defined on top of the basic +syntax. Note that in many cases, their expansions are defined recursively or in +terms of other derived form. + +``` + (types) + T ::= ... + (T1, ..., Tn) ~> {_1 : T1, ..., _n : Tn} + T1 -> T2 ~> (_ : T1) -> T2 + T1 => T2 ~> (_ : T1) => T2 + P -> T ~> ($ : TP) -> let P in T [2] + P => T ~> ($ : TP) => let P in T [2] + T with .Xs A1 ... An = E ~> T with .Xs = fun A1 ... An => E + T with type .Xs A1 ... An = T' ~> T with .Xs = fun A1 ... An => type T' + let B in T ~> (let B in type T) + rec P => T ~> (rec P => type T) + + (arguments) + A ::= + (X : T) + '(X : type) + '(type X) ~> '(X : type) + 'X ~> '(X : type) + X ~> (X : _) or (X : type) [1] + P + + (declarations) + D ::= ... + X A1 ... An : T ~> X : A1 -> ... -> An -> T + X A1 ... An = E ~> X : A1 -> ... -> An -> (= E) + type X A1 ... An ~> X : A1 => ... => An => type + type X A1 ... An = T ~> X : A1 => ... => An => (= type T) + local B in D end ~> include (let B in {D}) + + (expressions) + E ::= ... + (E1, ..., En) ~> {_1 = E1, ..., _n = En} + E.i ~> E._i + fun P => E ~> fun ($ : TP) => let P in E [2] + fun A1 ... An => E ~> fun A1 => ... => fun An => E + (.X) ~> fun Y => Y.X + (SYM) ~> SYM + E1 SYM E2 ~> (SYM) (E1, E2) [3] + if E1 then E2 else E3 ~> if E1 then E2 else E3 : _ + E1 or E2 ~> if E1 then true else E2 + E1 and E2 ~> if E1 then E2 else false + E : T ~> (fun (X : T) => X) E + E :> T ~> unwrap (wrap E : T) : T + let B in E ~> {B ; X = E}.X + rec P => E ~> rec (X : TP) => let P = X in E [2] + do E ~> let _ = E in () + (E1; ...; En) ~> do {do E1; ...; do En} + + (patterns) + P ::= + _ ~> (; empty ;) + X ~> X = $ + {X1 = P1, ..., Xn = Pn} ~> P1 = $.X1; ...; Pn = $.Xn + {..., X, ...} ~> {..., X = X, ...} + {..., X : T, ...} ~> {..., X = X : T, ...} + {..., X : T = E, ...} ~> {..., X = E : T, ...} + {..., type X A1 ... An, ...} ~> {..., X : A1 => ... => An => type, ...} + (P1, ..., Pn) ~> {_1 = P1, ..., _n = Pn} + (type X A1 ... An) ~> (X : A1 => ... => An => type) + wrap P : T ~> local $ = unwrap $ : T in P = $ end + @T P ~> local $ = $.@T in P = $ end + P : T ~> P = $ : T + P1 as P2 ~> P1; P2 + + (bindings) + B ::= ... + X ~> X = X + P = E ~> local $ = E in P end + X A1 ... An = E ~> X = fun A1 ... An => E + X A1 ... An : T = E ~> X = fun A1 ... An => E : T + X A1 ... An :> T = E ~> X = fun A1 ... An => E :> T + type X A1 ... An = T ~> X = fun A1 ... An => type T + local B1 in B2 end ~> include (let B1 in {B2}) + do E ~> local _ = E in end +``` + +Note [1]: The expansion of an argument `X` to `(X : type)` is only used for the +arguments to a `type'` declaration or binding, in all other places it is treated +as `(X : \_)`. + +Note [2]: The type `TP` is derived from the pattern `P` as follows: + +``` + _ ~> _ + X ~> _ + { X1 = P1, ..., Xn = Pn } ~> { X1 : TP1; ...; Xn : TPn } + wrap P : T ~> T as wrap TP + @T P ~> T as (rec _ => type TP) + P : T ~> TP as T + P1 as P2 ~> TP1 as TP2 +``` + +Note [3]: There is currently no precedence rules for infix operators, they are +all left-associative with the same precedence. + +### Notes on Specific Constructs + +Much of the syntax should hopefully is self-explanatory if you are familiar with +ML. Here are a few less obvious bits. + +#### Evaluating Expressions and Printing + +Programs consist of bindings, and the prompt expects bindings, too. To evaluate +an expression for its side effect, the 'do' notation can be used: + +``` + do Int.print (3 + 5); +``` + +Here, `Int.print` is defined in [prelude.1ml](prelude.1ml). The prompt does not +currently print results itself. + +#### Type Definitions + +Types can be defined in a familiar style using the respective sugar: + +``` + type t = int; ;; t = type int + type pair x y = (x, y); ;; pair = fun (x : type) => fun (y : type) => (x, y) + + type MONAD (m : type => type) = + { + return 'a : a -> m a; + bind 'a 'b : m a -> (a -> m b) -> m b; + }; + + type SIG = + { + type t; ;; t : type + type u a; ;; u : (a : type) => type + type v = int; ;; v : (= type int) + type w a (c : type => type) = (u a, c t); + ;; w : (a : type) => (c : (_ : type) => type) => (= type {_1: u a, _2: c t}) + }; +``` + +#### Implicit Polymorphism + +Types are generalised Damas/Milner-style at bindings: + +``` + pair x y = {fst = x; snd = y}; + p = pair 5 "foo"; +``` + +The type of pair can be declared as follows: + +``` + pair 'a 'b : a -> b -> {fst : a; snd : b} +``` + +which is just sugar for + +``` + pair : 'a => 'b => a -> b -> {fst : a; snd : b} +``` + +or even more explicitly, + +``` + pair : '(a : type) => '(b : type) => a -> b -> {fst : a; snd : b} +``` + +Generalisation can also take place as part of subtyping (a.k.a. signature +matching), e.g. in the following example: + +``` + f (id : ‘a => id -> id) = (id 5, id “”) + p = f (fun x => x) +``` + +This also shows that implicit functions naturally are first-class values. + +#### Recursive Types + +There are no datatype definitions, recursive types have to be defined +explicitly, and require explicit injection/projection. + +``` + type stream = rec t => {hd : int; tl : () -> opt t}; ;; creates rec type + single x = @stream{hd = x; tl = fun () => none}; ;; @(t) e rolls value into t + @stream{hd = n} = single 5; ;; @(t) p pattern matches on rec value + do Int.print n; ;; or: + do Int.print (single 7 .@stream .hd); ;; e.@(t) unrolls rec value directly +``` + +#### Recursive Functions + +The `rec` expression form allows defining recursive functions: + +``` + count = rec self => fun i => + if i == 0 then () else self (i - 1); + + repeat = rec self => fun x => + @stream{hd = x; tl = fun () => some (self x)}; +``` + +Mutual recursion is also expressible: + +``` + {even; odd} = rec (self : {even : int -> stream; odd : int -> stream}) => + { + even x = @stream{hd = x; tl = fun () => some (self.odd (x + 1))}; + odd x = @stream{hd = x; tl = fun () => some (self.even (x + 1))}; + } +``` + +Unfortunately, there is no nicer syntax for recursive declarations yet. + +#### Impredicative Polymorphism + +By default, polymorphism is predicative in 1ML. That is, abstract types can only +be matched by "small" types (types not containing abstract types themselves). +However, it is possible to inject large types into the small universe +explicitly, using `wrap` types. From [prelude.1ml](prelude.1ml): + +``` + type OPT = + { + type opt a; + none 'a : opt a; + some 'a : a -> opt a; + caseopt 'a 'b : opt a -> b -> (a -> b) -> b; + }; + Opt :> OPT = + { + ;; Church encoding; it requires the abstract type opt a to be implemented + ;; with a polymorphic (i.e., large) type. Thus, wrap the type. + type opt a = wrap (b : type) => b -> (a -> b) -> b; + none = wrap (fun (b : type) (n : b) (s : _ -> b) => n) : opt _; + some x = wrap (fun (b : type) (n : b) (s : _ -> b) => s x) : opt _; + caseopt xo = (unwrap xo : opt _) _; + }; +``` + +Note how values of type `wrap T` have to be wrapped and unwrapped explicitly, +with a type annotation.