Created
August 17, 2023 22:51
-
-
Save fogti/fb61cd871a0f65dcf6e2ff8f8fbb08be to your computer and use it in GitHub Desktop.
possible Yanais introductory example (proglang planning phase)
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* | |
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... *) | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment