This paper defines an extended polymorphic type system for an ML-style programming language, and develops a sound and complete type inference algorithm. Different from the conventional ML type discipline, the proposed type system allows full rank 1 polymorphism, where polymorphic types can appear in other types such as product types, disjoint union types and range types of function types.
namespace system (
interface num = #a where (
def plus: a -> a -> a
def min: a -> a -> a
def mul: a -> a -> a
def div: a -> a -> a
)
def +: ::num a => a -> a -> a =
\x,y -> x.plus x y
def -: ::num a => a -> a -> a =
\x,y -> x.min x y
def *: ::num a => a -> a -> a =
\x,y -> x.mul x y
def /: ::num a => a -> a -> a =
\x,y -> x.div x y
)
namespace system (
interface ord = #a where (
def compare: a -> a -> int
)
def ==: ::ord a => a -> a -> bool =
\x,y -> int_eq (x.compare x y) 0
def <: ::ord a => a -> a -> bool =
\x,y -> int_less (x.compare x y) 0
def <=: ::ord a => a -> a -> bool =
\x,y -> int_less (x.compare x y) 1
def >: ::ord a => a -> a -> bool =
\x,y -> int_less (x.compare y x) 0
def >=: ::ord a => a -> a -> bool =
\x,y -> int_less (x.compare y x) 1
)
namespace system (
type bool = [ true | false ]
def not: bool -> bool =
[ true -> false
| _ -> true ]
def and: bool -> bool -> bool =
[ true, true -> true
| _ , __ -> false ]
def or: bool -> bool -> bool =
[ false, false -> false
| _ , __ -> true ]
def eq: bool -> bool -> bool =
[ false, false -> true
| true , true -> true
| _ , __ -> false ]
instance ord bool where (
def compare: bool -> bool -> int =
[ false, false -> 0
| true, true -> 0
| false, _ -> 0-1 ]
)
)
namespace system (
// type int = [ MININT | ... | -1 | 0 | 1 | 2 | ... | MAXINT ]
type int = {system.int}
def int_monadic_min: int -> int =
\v0 -> {int_monadic_min[v0]}
def int_dyadic_min: int -> int -> int =
\v0,v1 -> {int_dyadic_min[v0,v1]}
def int_plus: int -> int -> int =
\v0,v1 -> {int_plus[v0,v1]}
def int_mul: int -> int -> int =
\v0,v1 -> {int_mul[v0,v1]}
def int_div: int -> int -> int =
\v0,v1 -> {int_div[v0,v1]}
def int_compare: int -> int -> int =
\v0,v1 -> {int_compare[v0,v1]}
def int_eq: int -> int -> bool =
\v0,v1 -> {int_eq[v0,v1]}
def int_less: int -> int -> bool =
\v0,v1 -> {int_less[v0,v1]}
def int_magic_tick: () -> bool =
\v0 -> {int_magic_tick[v0]}
instance num int where (
def plus: int -> int -> int = int_plus
def min: int -> int -> int = int_dyadic_min
def mul: int -> int -> int = int_mul
def div: int -> int -> int = int_div
)
instance ord int where (
def compare: int -> int -> int = int_compare
)
)
namespace system (
type char = {system.char}
def char_compare: char -> char -> char =
\v0,v1 -> {char_compare[v0,v1]}
def char_eq: char -> char -> bool =
\v0,v1 -> {char_eq[v0,v1]}
def char_less: char -> char -> bool =
\v0,v1 -> {char_less[v0,v1]}
def char_ascii_code: char -> int =
\v0 -> {char_ascii_code[v0]}
def char_ascii_char: int -> char =
\v0 -> {char_ascii_char[v0]}
instance ord char where (
def compare: char -> char -> int = char_compare
)
)
namespace system (
def file_read: list char -> list char =
\v0 -> {file_read[v0]}
def file_write: list char -> list char -> unit =
\v0,v1 -> {file_write[v0,v1]}
)
namespace list (
using system
type list = \a => [nil | cons a (list a)]
instance ord (list a) where (
def compare: ::ord a => int =
[ nil , nil -> 0
| nil , _ -> 0-1
| _ , nil -> 1
| cons x xx, cons y yy ->
if x == y then xx.compare xx yy
else x.compare x y ]
)
def concat: list a -> list a -> list a =
[ nil, yy -> yy
| cons x xx, yy -> cons x (concat xx yy) ]
def map: (a -> b) -> list a -> list b =
[ f, nil -> nil
| f, cons x xx -> cons (f x) (map f xx) ]
def head: list a -> list a = [ cons x xx -> x ]
def tail: list a -> list a = [ cons x xx -> xx ]
)
namespace system (
type tuple_2_t = \t0 => \t1 => [tuple_2 t0 t1]
instance ::ord t0 => ::ord t1 => ord (tuple_2 t0 t1) where (
def compare: tuple_2_t t0 t1 -> tuple_2_t t0 t1 -> int =
[ tuple_2 x0 x1, tuple_2 y0 y1 ->
let c = x0.compare x0 x1 in
if c == 0 then x1.compare x1 y1 else c ]
)
type tuple_3_t = \t0 \t1 \t2 => [tuple_3 t0 t1]
)
/* Some example programs */
using system
using list
def fac: int -> int =
[ 0 -> 1
| 1 -> 1
| n -> n * (fac (n - 1)) ]
def collatz: int -> int =
let even = [n -> (n / 2) * 2 == n] in
[ 1 -> 1
| n -> if even n
then collatz (n / 2)
else collatz (1 + (n * 3)) ]
def fibs: int -> list int =
[ 0 -> cons 1 (cons 1 nil)
| n -> let ff = fibs (n-1) in
cons (head ff + (head (tail ff))) ff]
def main: (int, list int) =
let f = [(x,y) -> y] in
let p = (let n = 3 in (n, fibs n)) in f p
---------------------------------------------------------
-- the "-{...}" means that we're going to do compile-time
-- stuff (here, syntax extension)
---------------------------------------------------------
-{ block:
------------------------------------------------------
-- Register the additional keywords in mlp.lexer
------------------------------------------------------
mlp.lexer:add{ "let", "in" }
------------------------------------------------------
-- Extend the expression parser; code generation is
-- delegated to the function let_in_builder() below.
------------------------------------------------------
mlp.expr:add{
"let", mlp.id, "=", mlp.expr, "in", mlp.expr,
builder = let_in_builder }
------------------------------------------------------
-- This creates the code returned by the macro.
-- Notice the holes-in-quote-in-splice.
------------------------------------------------------
local function let_in_builder (x)
local variable, value, expr = unpack (x)
return +{
function (-{variable})
return -{expr}
end (-{value}) }
end
} -- back to "normal" code
a, b, c = 1, 1, -2
roots = let sqrt_delta = (b^2-4*a*c)^0.5 in
{ (sqrt_delta-b)/(2*a), (-sqrt_delta-b)/(2*a) }
SML# supports the following practically important new features:
SML# is carefully designed so that
Currently, SML# (0.20 release version) is available in the following forms.
“After a long and careful analysis the results are clear: 11 out of 10 people can't handle threads.”
Todd Hoff
Recall the definition of S:
S : (A -> B -> C) -> (A -> B) -> A -> C
S = λ x y a -> x a (y a)
I am assuming a simple semantics of sets and functions, and by S being injective I mean that S x = S x' ⇒ x = x', which can be trivially shown below:
S x = S x'
≡ { η expansion, for all y : A -> B, a : A }
(∀ a, y : S x y a = S x' y a)
≡ { definition of S }
(∀ a, y : x a (y a) = x' a (y a))
⇒ { choose y = K b for some b }
(∀ a, b : x a (K b a) = x' a (K b a))
≡ { definition of K: K b a = b }
(∀ a, b : x a b = x' a b)
≡ { pointwise equality }
x = x'
Now that we know S is injective, there ought to exist some function S⁻¹ such that S⁻¹ ○ S = id. Nakano san claimed that a definition would be:
S⁻¹ : ((A -> B) -> A -> C) -> A -> B -> C
S⁻¹ = λ x a b -> x (K b) a
That S⁻¹ ○ S = id is easy to see:
S⁻¹ (S x) a b
= (S x) (K b) a
= x a (K b a)
= x a b
From another direction, we have only S ○ S⁻¹ ⊆ id since S is not a surjective function. How the range of S look like? Inspecting the definition of S. Since y is applied only once to a, the value of y on other input does not matter. That is, the range of S consists of only functions e such that:
e y a = e y' a for all y, y' such that y a = y' a ......(1)
We will show that S (S⁻¹ e) = e for all e satisfying (1):
S (S⁻¹ e) y a
= { definition of S }
S⁻¹ e a (y a)
= { definition of S⁻¹ }
e (K (y a)) a
= { by (1), since K (y a) a = y a }
e y a
Some endnotes. Once Nakano and I thought we discovered how to invert higher-order functions (and even derive the necessary side conditions, like the one on e above) by drawing λ expressions as trees and manipulating them. It turned out that I overlooked something obvious in the very beginning and the result was a disaster.
