Skip to content

Instantly share code, notes, and snippets.

@sgoguen
sgoguen / FiniteTypes.Lean
Last active December 18, 2023 19:32
Counting Types with Lean
import MIL.Common
import Mathlib.Data.Nat.Pairing
-- Let's define a type that represents all finite types
-- Taken from (A Universe of Finite Types - Functional Programming in Lean)
-- https://lean-lang.org/functional_programming_in_lean/dependent-types/universe-pattern.html
inductive FiniteType where
| unit : FiniteType
| bool : FiniteType
| pair : FiniteType → FiniteType → FiniteType
@sgoguen
sgoguen / person-or-cheese.fs
Created December 6, 2023 00:46
Person or Cheese - Type Inferencing
type Person = { Name: string; Age: int }
type Cheese = { Name : string; Age : int }
let people = [
{ Name = "Brie"; Age = 30 }
{ Name = "Colby"; Age = 20 }
{ Name = "Jack"; Age = 40 } ]
let printName thing = thing |> _.Name |> printfn "%s"
people[0] |> printName
@sgoguen
sgoguen / compose-total.fs
Created February 7, 2023 05:53
Composing Total Recursive Functions
let composeRecursive baseF recursiveFs =
let funcs = [| (fun _ x -> baseF x); yield! recursiveFs |]
let length = bigint(Array.length funcs)
let rec natToObject n =
let r = int(n % length)
let recF = funcs[r]
let f = recF natToObject
f (n / length)
natToObject
@sgoguen
sgoguen / recursive-active-patterns.fs
Created January 10, 2023 21:21
Converting Natural Numbers to Recursive Data Structures with Active Patterns
module NatPatterns =
type nat = int64
let nat(x) = int64(x)
// Rosenberg-Strong unpairing function (balances better than Cantor's)
// A true total function when you replace int64 with bigint
let unpair(z: nat): (nat * nat) =
let m = nat(floor (sqrt (double z)))
let ml = z - (m * m)
@sgoguen
sgoguen / Reader.fsx
Created December 7, 2022 19:03
F# Reader Monad Example
type Reader<'Env, 'T> = Reader of ('Env -> 'T)
module Reader =
let run (Reader f) env = f env
let ret x = Reader(fun _ -> x)
let ask = Reader(fun env -> env)
let zero() = Reader(fun _ -> ())
let map f (Reader g) = Reader(fun env -> f (g env))
let delay (f: unit -> Reader<'TEnv, 'T>) =
Reader(fun env -> run (f()) env)
@sgoguen
sgoguen / text-davinci-003.md
Last active December 1, 2022 18:26
GPT-3.5 Teaching me F#

My First Conversation with GPT-3.5

The following is a conversation with an AI assistant. The assistant is helpful, creative, clever, and very friendly.

Human: Hello, who are you?

AI: I am an AI created by OpenAI. How can I help you today?

Human: Can you help me write an F# tutorial?

@sgoguen
sgoguen / mapping-n-to-expressions.py
Last active July 28, 2022 16:22
A bijective map from the set of natural numbers to the set of equations
def pair(x, y):
mxy = max(x, y)
return mxy * mxy + mxy + x - y
def unpair(z):
m = int(z ** 0.5)
ml = z - m * m
if ml < m:
@sgoguen
sgoguen / map-ala-hack.ts
Last active September 7, 2021 21:26
A Hack Styled Operator
type Func<A, B> = (input: A) => B;
const _$ = undefined;
// If f and the input are provided, evalulate and return B[]
function map<A, B>(input: A[], f: Func<A, B>): B[];
// If input is not provided, return a function ala partial application
function map<A, B>(input: undefined, f: Func<A, B>): Func<A[], B[]>;
function map<A, B>(input: A[] | undefined, f: Func<A, B>) {
type Moves = int
type ActionRoll =
| CheckOneCamera
| MotionSensor // Tells you which camera the thief is on
| ScanAll
type WindowState = Locked | Open
type Square = {
class A {
keya = "a" as const;
}
class B {
keyb = "b" as const;
}
// Turned your class map into a constructor map to simplify it.
const classMap = {
'a': () => new A(),