Git Product home page Git Product logo

mlsr's Introduction

MLSR

MLSR is an interpreter of a functional programming language that supports let-polymorphism, Hindley-Milner type inference, and polymorphic algebraic effects and handlers with signature restriction, which is a methodology to restrict type interfaces of algebraic effects for type-safe handling of polymorphic effects. MLSR is a polymorphic effectful call-by-value (CBV) language, but it does not need to enforce value restriction—which is another approach to reconciling polymorphism and computational effects in CBV languages (or fragments) and is adopted by other many ML-like languages including OCaml, Standard ML, Koka, etc.—thanks to the signature restriction. The details including formalization and metatheory are found at our paper:

  • Taro Sekiyama, Takeshi Tsukada, and Atsushi Igarashi: Signature restriction for polymorphic algebraic effects. Conditionally accepted at ICFP 2020. Preprint: https://arxiv.org/abs/2003.08138

This artifact is an implementation of the extended type system in Sections 4 & 5 of our paper, and does not support the type-and-effect system in Section 6.

Getting started

Requirements

  • ocaml (>= 4.10)
  • opam (>= 2.0)
  • dune (>= 2.5)
  • menhir
  • ppx_deriving (>= 4.4.1)
  • ounit2 (>= 2.2.2) (for tests)

All packages can be installed via opam.

Building from source code

$ dune build
$ ./_build/install/default/bin/mlsr

Installation via opam

$ opam install .
$ mlsr

Example files

The directory examples contains the example files listed below.

  • readme.mlsr : All of the examples described in the example section below
  • 2.1.mlsr : The examples in Section 2.1 of our paper
  • 2.2.mlsr : The example in Section 2.2
  • 2.3.mlsr : The (ill-typed) example in Section 2.3
  • 4.5_remark1.mlsr : The (ill-typed) example in Remark 1 (Section 4.5).
  • 5.2.mlsr : The example in Section 5.2

Our interpreter does not support file loading directly, but one can run the program in a file by:

$ cat [file path] | mlsr

Tips

User-firendly interface

Our interpreter does not support user-friendly line editing and input history search directly, but one can make use of such features via rlwrap.

$ rlwrap mlsr

Disabling signature restriction

Checking the signature restriction can be disabled by specifying the option --disable-signature-restriction in starting up the interpreter. Note that this option makes type-unsafe programs well typed badly; see below for detail.

$ mlsr --disable-signature-restriction

Running tests

The following command will run all of the tests in the directory test.

$ dune runtest

Directories

  • bin : Entry point of the interpreter
  • lib : Implementation of the interpreter
  • test : Unit tests
  • examples : Examples

Syntax

The syntax of MLSR is given by the following BNF. We write A* for (possibly empty) lists of elements in the class A. (For example, x* represent sequences of variables.) \mid is replaced by | in program code. Texts surrounded by (* and *) are just comments. We may emphasize nonterminal symbols by wrapping them with __ (e.g., __integers__for integer literals).

Term variables ::= x, y, z, f, g, k, op, etc.
Type variables ::= 'a, 'b, 'c, etc.

Top-level ::= ED ;; | VD ;; | e ;;

Effect declarations ED ::= effect op : 'a* . T1 => T2

Types T ::= 'a         (* Type variables *)
          | BT         (* Base types *)
          | T1 -> T2   (* Function types *)
          | T1 * T2    (* Product types *)
          | T1 + T2    (* Sum types *)
          | T list     (* List types *)

Base Types BT ::= bool | int | string | float | unit

Variable declarations VD ::= let x y* = e | let rec f x y* = e

Expressions e ::= x
                | c
                | fun x y* -> e | e1 e2 |
                | let x y* = e1 in e2 | let rec f x y* = e1 in e2
                | ( e1 , e2 ) | inl e | inr e

                (* the empty list and cons; syntax sugar for lists [ e1 ; ... ; en ] is supported *)
                | [] | e1 :: e2 |

                | match e with p
                | if e1 then e2 else e3 | e1 ; e2
                | handle e with { return x -> x ( \mid o )* }

Constants c ::= () | true | false | __integers__ | __floating-point numbers__ | __strings__
              | __primitive operations__   (* see the examples below for detail *)

Pattern clauses p ::= ( x , y ) -> e
                    | inl x -> e1 \mid inr y -> e2
                    | [ ] -> e1 \mid x :: y -> e2

Operation clauses o ::= op x k -> e

Examples

The following examples can also be found at the file examples/readme.mlsr.

Functions

# let plus42 = fun x -> x + 42;;
val plus42 : int -> int = <fun>

# plus42 1;;
val - : int = 43

# let plus42 x = x + 42;;
val plus42 : int -> int = <fun>

# plus42 3;;
val - : int = 45
# let rec fact n = if n = 0 then 1 else n * fact (n - 1);;
val fact : int -> int = <fun>

# fact 10;;
val - : int = 3628800

Let-polymorphism

# let id x = x;;
val id : 'a -> 'a = <fun>

# id true;;
val - : bool = true

# id 0;;
val - : int = 0

# let f x = x in (f true, f 0);;
val - : bool * int = (true, 0)

MLSR is free from the value restriction.

# let f = id id in (f "foo", f 1);;
val - : string * int = ("foo", 1)

The value restriction does not accept the expression above because f could not have a polymorphic type under it.

Pairs, injections, and lists

# let x = (1, "foo");;
val x : int * string = (1, "foo")

# match x with (y, z) -> y + str_len z;;  (* str_len returns the length of a string *)
val - : int = 4
# let f x = match x with inl x -> x = 0 | inr y -> y;;
val f : int + bool -> bool = <fun>

# f (inl 5);;
val - : bool = false

# f (inr true);;
val - : bool = true
# let rec length x = match x with [] -> 0 | y::ys -> 1 + length ys;;
val length : 'a list -> int = <fun>

# length [true];;
val - : int = 1

# length [1;2;3];;
val - : int = 3

Algebraic effect handlers

To invoke effects in MLSR, we first need to declare effect operations.

(* Declares effect operation select,
   which can be referred to as a variable of polymorphic type 'a list -> 'a *)

# effect select : 'a . 'a list => 'a;;
effect select : 'a list -> 'a defined

# select;;
val - : 'a list -> 'a = <fun>

(* The following expression is well typed
   but its evaluation terminates at the "Uncaught continuation" error as expected *)

# select [1;2;3];;
Run-time error: Uncaught continuation

Effect operations are handled by handlewith expressions. For example, the following code handles select and returns the head of a given list as a result of the call to select.

# handle 42 + select [1;2;3] with {
    return x -> x
  | select x k -> (match x with [] -> -1 | y::ys -> k y)
  };;
val - : int = 43

The return clause handles the evaluation result of the handled expression.

# handle 42 with { return x -> x * 10 };;
val - : int = 420

Continuations given to the operation clause are wrapped by the handler installed at the handlewith expression. For example, in the following code, the continuation k is invoked with the head of the argument list (i.e., 1) and then the continuation will perform the remaining computation (42 + 1) and pass the result to the return clause. Thus, the final result is 430.

# handle 42 + select [1;2;3] with {
    return x -> x * 10
  | select x k -> (match x with [] -> -1 | y::ys -> k y)
  };;
val - : int = 430

We also can collect all of the values computed with elements in the list.

# let rec map l f = match l with [] -> [] | x::xs -> (f x) :: (map xs f);;
val map : 'a list -> ('a -> 'b) -> 'b list = <fun>

# let rec append l m = match l with [] -> m | x::xs -> x :: (append xs m);;
val append : 'a list -> 'a list -> 'a list = <fun>

# let rec concat l = match l with [] -> [] | x::xs -> append x (concat xs);;
val concat : 'a list list -> 'a list = <fun>

# handle 42 + select [1;2;3] with { return x -> [x] | select x k -> concat (map x k) };;
val - : int list = [43; 44; 45]

In the operation clause, x is assigned type 'a list where 'a is a locally assigned type variable and must not be escaped from the operation clause.

# handle 42 with { return x -> x | select x k -> x };;
Typing error: Type variables bound in an operation clause cannot be escaped

Handlers can deal with two or more operation clauses.

# effect fail : 'a. unit => 'a;;
effect fail : unit -> 'a defined

# let f xs ys = handle
      let x = select xs in
      let y = select ys in
      if y = 0 then fail () else x / y
    with {
      return z -> [z]
    | select x k -> concat (map x k)
    | fail x k -> []
    };;
val f : int list -> int list -> int list = <fun>

# f [42; 12; 6] [3;2;0];;
val - : int list = [14; 21; 4; 6; 2; 3]

Signature restriction

By default MLSR checks if a declared effect follows the signature restriction for ensuring type safety. For example, the following get_id, which is an example used in our paper, is rejected because it invalidates the signature restriction.

# effect get_id : 'a. unit => 'a -> 'a;;
Typing error: The type signature does not follow the signature restriction on the codomain type

In general, the signature restriction requires quantified type variables ('a above) not to appear (1) at a non-strictly positive position in the domain type (unit above) nor (2) at a negative position in the codomain type ('a -> 'a above). See the paper for detail.

Disabling the signature restriction (unsafe)

We can disable the signature restriction by giving option --disable-signature-restriction to mlsr. Then, we can find the (ab)use of get_id gives rise to an undesired run-time error (as expected).

$ mlsr --disable-signature-restriction
# effect get_id : 'a. unit => 'a -> 'a;;
effect get_id : unit -> 'a -> 'a defined

# handle let f = get_id () in f 2; (f true) && false with {
    return x -> x
  | get_id x k -> k (fun y -> k (fun z -> y); y)
  };;
Run-time error: Operator "&&" can be applied only to Booleans

Here, f true is expected to return a Boolean, but at run-time it may return integer 2 for the lack of any restriction.

Below is the example in Remark 1 of the paper, showing the need of the restriction on domain types.

# effect op : 'a. ('a -> int) -> 'a => 'a;;
effect op : (('a -> int) -> 'a) -> 'a defined

# let v f x = inr (f (fun y -> inl x));;
val v : (('a -> 'b + 'c) -> 'd) -> 'b -> 'e + 'd = <fun>

# let n x = match x with inl y -> (if y then 0 else 1) | inr z -> z + 1;;
val n : bool + int -> int = <fun>

# handle let g = op(v) in match g 0 with inl z -> z | inr z -> n (g true) with {
    return x -> x
  | op x k -> k (x k)
  };;
Run-time error: Operator "+" can be applied only to integers

Complete list of primitive functions

(* Integers *)
# 1 + 2;;
# 6 - 4;;
# 4 * 5;;
# 7 / 2;;    (* n / 0 will cause a run-time error *)
# 11 % 3;;   (* n % 0 will cause a run-time error *)

(* Floating-point numbers *)
# 1.1 +. 2.4;;
# 5.8 -. 1.7;;
# 4.2 *. 2.;;
# 4.5 /. 1.5;;

(* Booleans *)
# true && false;;
# false || true;;
# if 1 = 2 then 3 else 4;;

(* Strings *)
# "foo" ^ "bar";;

(** `str_len s` returns the length of string `s` **)
# str_len "foo";; 

(** `str_sub s start len` returns the substring of `s`
    that starts at position `start` and has length `len`.
    Invalid arguments will cause a run-time error.
**)
# str_sub "foobar" 1 3;;

(* Lists *)
# [];;
# 1 :: 2 :: [];;
# [1.; 2.; 3.];;

(* Polymorphic comparison; comparing functions will fail  *)
# 1 = 2;;
# 1 <> 2;;
# 1.1 > 1.1;;
# 1.1 >= 1.1;;
# "foo" < "bar";;
# "foo" <= "bar";;

(* Sequential composition *)
# 1; true;;

mlsr's People

Contributors

skymountain avatar

Watchers

 avatar  avatar

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.