brendanzab

#![allow(dead_code)]

#[derive(Debug, Copy, Clone, PartialEq, Eq)]
enum Type {
    Unit,                               // ()
    Int,                                // Int
    Float,                              // Float
}

type Expr = Box<ExprNode>;

brendanzab

(** This is a demonstration of implementing interpreters in an extensible way
    that offers a partial solution to the expression problem. The idea is that
    the language can be extended with more features after the fact, without
    altering previous definitions. It also has the benefit of grouping the
    related extensions to the syntax and semantic domains together with the
    relevant evaluation rules in a per-feature way.

    This approach used is similar to the one described by Matthias Blume in
    {{:https://www.microsoft.com/en-us/research/video/records-sums-cases-and-exceptions-row-polymorphism-at-work/}
    Records, sums, cases, and exceptions: Row-polymorphism at work}.

brendanzab

// WARNING: I have never programmed in gleam before and this is probably 
// considered very unideomatic/cursed. You have been warned! :P

import gleam/io
import gleam/option.{type Option, None, Some}

type Iterator(a) {
  Iterator(next: fn () -> Option(#(a, Iterator(a))))
}

brendanzab

(* Based on https://effekt-lang.org/examples/comefrom.html *)

module ComeFrom () : sig

  val label : unit -> unit (* Label *)
  val try_with : ?label:(unit -> unit (* E *)) -> ('a -> 'b (* Label *)) -> 'a -> 'b (* E *)

end = struct

  type 'a Effect.t += Label : unit Effect.t

brendanzab

-- ------------------------------- --
-- Base types                      --
-- ------------------------------- --

data Top {
    Unit,
}

data Bot { }

brendanzab

-- ------------------------------- --
-- Non-dependent functions         --
-- ------------------------------- --

codata Fun(a b: Type) {
    Fun(a, b).ap(a b: Type, x: a) : b,
}

-- ------------------------------- --
-- Top type                        --

brendanzab

use std::hash::Hash;

pub trait Key {
  type T: Hash + Eq;
}

pub trait Map<K : Key> {
  type T<V>;

  fn new<V>() -> Self::T<V>;

brendanzab

(* inspired by https://github.com/Tobi-3/build-systems-a-la-carte-with-effect-handlers/*)

type key = string
type value = int

type _ Effect.t +=
  | Fetch : key -> value Effect.t
  | NeedInput : key -> value Effect.t
  | GetValue : key -> value option Effect.t
  | SetValue : key * value -> unit Effect.t

brendanzab

(** Fractal binary trees

    L-systems are a really wonderful model of plant growth, showing how a set of
    simple grammar rules can result in incredibly life-like and complicated
    organic forms.

    They do however seem a little… stuck in the 80s? In L-systems the state of a
    plant is modelled as a list of instructions, where the branching structure
    emerges from an imperative interpretation of “push” and “pop” symbols. For
    example an L-system that describes a fractal binary tree looks like this:

brendanzab

(*
  T ::=
    | Bool
    | T -> T

  t ::=
    | x
    | \(x : T). t
    | t t