Skip to content

Instantly share code, notes, and snippets.

View HarrisonGrodin's full-sized avatar

Harrison Grodin HarrisonGrodin

View GitHub Profile
@HarrisonGrodin
HarrisonGrodin / style-guide.md
Last active October 21, 2021 22:38
Standard ML style guide

Standard ML Style Guide

Core Language

atexp

Special Constant: <scon>

<scon>
@HarrisonGrodin
HarrisonGrodin / dynamic-dispatch.sml
Created August 13, 2021 06:13
Simple model of Python-style dynamic dispatch in Standard ML via dynamic classification
signature OBJECT =
sig
type 'a tag
type t
val new : unit -> t list tag
and make : 'a tag -> 'a -> t
val get : t -> 'a tag -> 'a
(* primitives *)
@HarrisonGrodin
HarrisonGrodin / julia.sml
Last active July 18, 2021 04:11
Simple model of the Julia language in Standard ML via dynamic classification
signature OBJECT =
sig
type 'a tag
type t
val Bool : bool tag
and Int : int tag
and String : string tag
val toString : t -> string
@HarrisonGrodin
HarrisonGrodin / FreeGroup.agda
Created July 11, 2021 02:49
The free group in Cubical Agda
{-# OPTIONS --cubical #-}
open import Cubical.Foundations.Prelude
infix 1 begin_
begin_ : {A : Set} {x y : A} → x ≡ y → x ≡ y
begin_ x≡y = x≡y
infix 9 _⁻¹
infixl 5 _·_
@HarrisonGrodin
HarrisonGrodin / univ_map.sml
Last active June 18, 2021 17:17
Universal map in Standard ML
signature UNIV_MAP =
sig
structure Key : sig
type 'a t
val create : unit -> 'a t
end
type t
val empty : t