Skip to content

Instantly share code, notes, and snippets.

Avatar
♥️
Laughing at the abysm

Eduardo Rafael EduardoRFS

♥️
Laughing at the abysm
View GitHub Profile
View values_are_proofs_types_are_propositions.ts
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;
View gadt_using.ts
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> };
View bad_gadt.ml
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
View class_is_structural.ml
class a =
object
method x = 1
end
class b =
object
method x = 2
end
View dump_cmi_414.ml
[@@@ocaml.warning "-32"]
module Location = struct
include Location
let pp = print_loc
end
module Longident = struct
include Longident
View dummy_ticket.ml
type _ ticket
type _ contract
type operation
type address
type nat
type mutez = int
module rec Tezos : sig
val create_ticket : 'value -> nat -> 'value ticket
View simple_mark.ml
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
View language-problems.md

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

View package-manager.md

Features

  • overalys should be a first class experience
View fixed_array.ml
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