EduardoRFS

type Eq<A, B> = <X>(a: A, eq: (x: A & B) => X) => X;
const refute = (x: never) => x;
const refl = <A, X>(a: A, eq: (x: A) => X) => eq(a);

const sickos = <A>(x: A, eq: Eq<A, number>) => eq(x, (x) => x);
const two = sickos(2, refl);

type Ty<A> =
  | { tag: "number"; eq: Eq<A, number> }
  | { tag: "string"; eq: Eq<A, string> };

EduardoRFS

module GADT = struct
  type 'a option = Some : 'a -> 'a option | None : 'a option

  let x = Some 1
  let y = None

  module Ty = struct
    type _ ty = Int : int ty | String : string ty

    let int = Int

EduardoRFS

class a =
  object
    method x = 1
  end

class b =
  object
    method x = 2
  end

EduardoRFS

[@@@ocaml.warning "-32"]

module Location = struct
  include Location

  let pp = print_loc
end

module Longident = struct
  include Longident

EduardoRFS

type _ ticket
type _ contract
type operation
type address
type nat
type mutez = int

module rec Tezos : sig
  val create_ticket : 'value -> nat -> 'value ticket

EduardoRFS

type value =
  | Block of block
  | Value of int
and block = {
  mutable marked : bool;
  fields : value array;
}

(* this doesn't work, fails when there is cycle and no progress *)
(* The idea here is that on each step we will be always traversing unmarked

EduardoRFS

Language Problems

Nominal Typing

Inference

Inference is weird for data types in OCaml due to modularity. Especially having records / variants with duplicated fields.

Solutions: weak subtyping

EduardoRFS

Features

• overalys should be a first class experience

EduardoRFS

module Fixed_array (P : sig
  val length : int
end) : sig
  type 'a t
  val length : 'a t -> int
  val make : 'a -> 'a t
  val get : 'a t -> int -> 'a
  val set : 'a t -> int -> 'a -> unit
end = struct
  type 'a t = 'a array

EduardoRFS

Instantiation in O(n)

Most of the time instantiation is actually O(n log n), this mostly don't matter as types are always small. But for big types by having an additional memory cell on every type, an array / vector can be created.

Invariants

Doesn't matter how forall is encoded, instantiation needs to copy all sections of a type that may include an occurence of the free variable being instantiated.

Maybe an additional branching can be used to prevent allocation.