possible Yanais introductory example (proglang planning phase)

yanais-00.yns

(*
  what language features do we want?

  * free tagged unions
  * dependent types
*)

mod Example {

pub tag True;
pub tag False;
pub const Bool = #[repr(int)] enum { True; False };

pub tag Some (t: *) = t;
pub tag None;
pub const Maybe (t: *) = enum { None; Some t };

(* unary numbers *)
pub tag Z;
pub tag S = UnaryNat;
pub const UnaryNat = #[repr(int)] enum { Z; S };

(* `Z` means the type, `#Z` means the associated tag *)

pub const List : (t: *) -> (n: UnaryNat) -> *
  = λ (t: *) -> {
      const TList = #[repr(array)] (λ (n: UnaryNat) -> match n {
        (* we associate the type None to an empty list *)
        #Z => None;
        (* technically, empty lists shouldn't have any type parameter, but that makes the usage cumbersome *)
        #S x => :{
          elem: t;
          next: TList x;
        };
      });
      TList
    };

pub const EList = (t: *) -> ∃ (n: UnaryNat) (List t n);

(* natural numbers in big-endian style, positive
   so we omit all leading 0s and the first 1
   for usability, the list is reversed *)

pub tag Nat = EList Bool;

pub const NullOrNat = enum { Null; Nat; };
pub tag Neg = Nat;
pub tag WholeNum = enum { Null; Nat; Neg; };

(* internal functions *)

const nat_prev_ : Bool -> ∃ (n: UnaryNat) (List Bool n) -> ∃ (m: UnaryNat) (List Bool m)
  = λ (b: Bool) -> λ #∃ (n: UnaryNat) (l: List Bool n) -> match b {
    (* 1...1 -> 1...0 *)
    #True => #∃ (#S n) #{ elem = #False; next = l; };
    #False => match n {
      (* 10 -> 1 *)
      #Z => #∃ #Z #None;
      (* 1...0 -> (prev 1...)1 *)
      #S pn => {
        const next_ = match l #{elem; next} => nat_prev_ elem pn next;
        match next_ (#∃ n _) -> (#∃ (#S n) #{ elem = #True; next = next_; })
      }
    };
  };

(* etc... *)

}