sgoguen

open System
open System.IO
open System.Collections.Generic

// Define a type to hold either a scalar or an image (2D array)
type Value =
    | Scalar of float
    | Array of float[,]  // 2D array representing the image

// Image size (for testing you might want to use a smaller value)

sgoguen

module Result

open System

type ResultBuilder() =
    member __.Return(x) = Ok x

    member __.ReturnFrom(m: Result<_, _>) = m

    member __.Bind(m, f) = Result.bind f m

sgoguen

(*
This is a port of the Haskell code from Paul Tarau's paper:

Everything Is Everything" Revisited: Shapeshifting Data Types with Isomorphisms and Hylomorphisms

Tarau, Paul. "" Everything Is Everything" Revisited: Shapeshifting Data Types with Isomorphisms and Hylomorphisms." Complex Systems 18.4 (2010): 475.

*)

type Iso<'A, 'B> = Iso of f: ('A -> 'B) * g: ('B -> 'A)

sgoguen

--- Tree Calculus

--- The following module defines the core operations of Barry Jay's original tree calculus.



--- For our purposes, we'll represent Δ as the ASCII letter l to represent a leaf.

--- Let's define the syntax of the TRIAGE calculus.
fmod TREE-CALC-SYNTAX is

sgoguen

//  The irony of this snippet is that Tree Calculus, unlike Lambda Calculus, is a 
//  system that was designed to be reflective so one doesn't have to resort to things
//  like Gödelian numbering systems or other schemes in order for it to reason about
//  its own programs.

//  But seeing how I know little to nothing about Tree Calculus, I figured this would be 
//  an interesting way to explore it.

//  Interestingly enough, this snippet was written one month before reading this post:
//  https://github.com/barry-jay-personal/blog/blob/main/2025-01-06-diagonal.md

sgoguen

//  Nerd sniped by Conor Mc Bride
//  https://github.com/pigworker/Samizdat/blob/main/Full.hs
//  Agda Proof - https://github.com/pigworker/Samizdat/tree/main/Full

//  I really have no idea what I'm doing here.

// The data type Fm is a syntax tree with nodes:
// V x = a variable reference
// Z   = zero (a canonical base value)
// D f = double the value represented by 'f'

sgoguen

namespace PolyTypeExample;

using PolyType;
using PolyType.Abstractions;
using PolyType.Examples.Utilities;

public class Examples
{
    // public static void 

sgoguen

Higher Order Functions Considered Unnecessary??

This is my conversation with my custom GPT. Beyond this point, my questions are in blockquotes, and the GPT's responses are in normal text.

Can you help me explain to my friend how higher-order functions can be replaced with parameterized modules? Here's the rub: I don't want you to do it with OBJ, I want you to show how to do it with parameterized modules in OCaml. FYI - He's an F# programmer, so you don't have to explain things like higher-order functions.

Here's the paper: https://cseweb.ucsd.edu/~goguen/pps/utyop.pdf

Hey Friend,

sgoguen

//  This is a fun experiement where we try reducing the amount of boilerplate code
//  to implement the more verbose types in gadt.ts

abstract class Exp<T> {
    abstract eval(): T;
}

/// Let's create a function that create a class that extends Exp
function createExp<TInput, T>(evalFn: (input: TInput) => T) {
    return class extends Exp<T> {

sgoguen

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