Type indexed values in 1ML

tiv.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;