Skip to content

Instantly share code, notes, and snippets.

@polytypic
Last active November 18, 2019 07:20
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save polytypic/cb6c6bc19126d35a09151e94c16e0232 to your computer and use it in GitHub Desktop.
Type indexed values in 1ML
;; Type indexed values in 1ML
;;
;; This is a very simple experiment at encoding type-indexed values in 1ML.
;;
;; Background:
;;
;; https://people.mpi-sws.org/~rossberg/1ml/
;; http://repository.readscheme.org/ftp/papers/zheyang-icfp98.pdf
;;
;; Run as:
;;
;; ./1ml prelude.1ml tiv.1ml
;; Signature for a Type Indexed Value definition
type TIV = {
type t a;
bool : t bool;
char : t char;
int : t int;
text : t text;
unit : t (type ());
list 'a : t a -> t (list a);
opt 'a : t a -> t (opt a);
alt 'a 'b : t a -> t b -> t (alt a b);
fn 'a 'b : t a -> t b -> t (type a -> b);
pair 'a 'b : t a -> t b -> t (type (a, b));
iso 'a 'b : (a -> b, b -> a) -> t b -> t a;
};
include {
Rep = {
type t a = wrap (v: TIV) -> v.t a;
local
nullary 'a (g: (v: TIV) -> v.t a) = wrap (fun (v: TIV) => g v) : t _;
in
bool = nullary (fun (v: TIV) => v.bool);
char = nullary (fun (v: TIV) => v.char);
int = nullary (fun (v: TIV) => v.int);
text = nullary (fun (v: TIV) => v.text);
unit = nullary (fun (v: TIV) => v.unit);
end;
local
unary 'a 'b (g: (v: TIV) -> v.t a -> v.t b) a =
wrap (fun (v : TIV) => g v ((unwrap a : t _) v)) : t _;
in
list = unary (fun (v: TIV) => v.list);
opt = unary (fun (v: TIV) => v.opt);
end;
local
binary 'a 'b 'c (g: (v: TIV) -> v.t a -> v.t b -> v.t c) a b =
wrap (fun (v: TIV) => g v ((unwrap a: t _) v) ((unwrap b: t _) v)) : t _;
in
alt = binary (fun (v: TIV) => v.alt);
pair = binary (fun (v: TIV) => v.pair);
fn = binary (fun (v: TIV) => v.fn);
end;
iso 'a 'b (aIb: (a -> b, b -> a)) b =
wrap (fun (v: TIV) => v.iso aIb ((unwrap b : t _) v)) : t _;
};
tiv 'a (v: TIV) (t: Rep.t a) = (unwrap t : Rep.t _) v;
} :> {
;; Value independent type representation combinators
Rep: TIV;
;; A helper to define a TIV
tiv 'a : (v: TIV) => Rep.t a -> v.t a;
};
;; A helper to avoid having to define all cases of a TIV
tivDefaults (t: type => type) (default: 'a => t a) : TIV = {
t = t;
bool = default;
char = default;
int = default;
unit = default;
text = default;
local
unary _ = default;
in
list = unary;
opt = unary;
end;
local
binary _ _ = default;
in
alt = binary;
fn = binary;
pair = binary;
end;
iso _ _ = default;
};
;; A type-indexed function to convert values to text
toText 'a : Rep.t a -> a -> text = tiv {
include tivDefaults (fun (t: type) => type t -> text) (fun _ => "<unimplemented>");
bool b = if b then "true" else "false";
unit () = "()";
text t = "\"" ++ t ++ "\"";
opt aT aO =
caseopt aO
(fun () => "none")
(fun a => "(some " ++ aT a ++ ")");
alt aT bT ab =
casealt ab
(fun a => "(left " ++ aT a ++ ")")
(fun b => "(right " ++ bT b ++ ")");
pair aT bT (a, b) = "(" ++ aT a ++ ", " ++ bT b ++ ")";
iso (ab, _) bT a = bT (ab a);
};
;; A type-indexed print (with line) function
println rep x = print (toText rep x ++ "\n");
;; Example invocations
local
include Rep
in
_ = println (int) 101;
_ = println (pair bool text) (true, "that");
_ = println (opt bool) (some false);
_ = println (iso (fun i => i <> 0, fun b => if b then 1 else 0) bool) 1;
end;
;; A recursive type and an encoding
;;type bools = rec (bools : type) =>
;; opt (pair bool bools);
;;
;;Rep = {
;; include Rep;
;;
;; bools =
;; rec (self : Rep.t _) => fun (v: TIV) => fun d =>
;; iso (fun r => r.@bools, fun n => @bools n)
;; (opt (pair bool self)) v d;
;;};
;;
;;local
;; someBools : bools = @bools (some (false, @bools (some (true, @bools none))));
;; include Rep;
;;in
;; _ = println bools someBools;
;;end;
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment