EduardoRFS

const one: number = 1;
const a: string = "a";
type Id = <A>(a: A) => A;
const id: Id = (a) => a;
type Apply = <A, B>(f: (a: A) => B, a: A) => B;
const apply: Apply = (f, a) => f(a);
type Never_implies_anything = <A>(a: never) => A;
const never_implies_everything = <A>(a: never) => a as A;
type Not<A> = (a: A) => never;
const not_never: Not<never> = (a) => a;

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