diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | Cargo.lock | 7 | ||||
| -rw-r--r-- | Cargo.toml | 6 | ||||
| -rw-r--r-- | LICENSE | 7 | ||||
| -rw-r--r-- | README.md | 1 | ||||
| -rw-r--r-- | src/ast.rs | 55 | ||||
| -rw-r--r-- | src/classes.rs | 3 | ||||
| -rw-r--r-- | src/effects.rs | 19 | ||||
| -rw-r--r-- | src/main.rs | 51 | ||||
| -rw-r--r-- | src/parser.rs | 6 | ||||
| -rw-r--r-- | src/simple.rs | 50 |
11 files changed, 206 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..ea8c4bf --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +/target diff --git a/Cargo.lock b/Cargo.lock new file mode 100644 index 0000000..2484e75 --- /dev/null +++ b/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "type-systems" +version = "0.1.0" diff --git a/Cargo.toml b/Cargo.toml new file mode 100644 index 0000000..6151d0f --- /dev/null +++ b/Cargo.toml @@ -0,0 +1,6 @@ +[package] +name = "type-systems" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html @@ -0,0 +1,7 @@ +BSD Zero Clause License + +Copyright (C) 2023 JJ <https://j-james.me> + +Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby granted. + +THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. diff --git a/README.md b/README.md new file mode 100644 index 0000000..cba6242 --- /dev/null +++ b/README.md @@ -0,0 +1 @@ +# a simple type system diff --git a/src/ast.rs b/src/ast.rs new file mode 100644 index 0000000..9202968 --- /dev/null +++ b/src/ast.rs @@ -0,0 +1,55 @@ +// Bidirectional type checking, simple types for effects (or perhaps subtyping?) and typeclasses + +use core::fmt; +use std::collections::HashMap; + +pub type Identifier = String; +pub type Context = HashMap<Identifier, Term>; + +// note: when comes the time, we'll put effects in here (i think) +#[derive(Clone, PartialEq, Eq)] +pub enum Expression { + Annotation{expr: Box<Expression>, kind: Type}, + Constant{term: Term}, + Variable{id: Identifier}, + Abstraction{param: Identifier, func: Box<Expression>}, + Application{func: Box<Expression>, arg: Box<Expression>}, + Conditional{if_cond: Box<Expression>, if_then: Box<Expression>, if_else: Box<Expression>} +} + +// _every_ type in our language is represented as this and interpreted as a type. +// how to store more data than fits... hmm +pub type Value = i8; + +#[derive(Debug, Copy, Clone, PartialEq, Eq)] +pub enum Type { + Empty, + Unit, + Bool, + Natural, + // Float, + // String, + // Enum(Vec<Type>), + // Record(Vec<Type>), + // Function{from: Box<Type>, to: Box<Type>}, +} + +// this means that functions cannot have types? unless we put them as empty values ig +#[derive(Debug, Copy, Clone, PartialEq, Eq)] +pub struct Term { + pub val: Value, + pub kind: Type, // currently useless / redundant: will be useful for casting +} + +impl fmt::Debug for Expression { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Expression::Annotation { expr, kind } => write!(f, "{:?}:{:?}", expr, kind), + Expression::Constant { term } => write!(f, "{}", term.val), + Expression::Variable { id } => write!(f, "{}", id), + Expression::Abstraction { param, func } => write!(f, "(λ{}.{:?})", param, func), + Expression::Application { func, arg } => write!(f, "{:?} {:?}", func, arg), + Expression::Conditional { if_cond, if_then, if_else } => write!(f, "if {:?} then {:?} else {:?}", if_cond, if_then, if_else), + } + } +} diff --git a/src/classes.rs b/src/classes.rs new file mode 100644 index 0000000..38a4847 --- /dev/null +++ b/src/classes.rs @@ -0,0 +1,3 @@ +// Typeclass pass: monomorphize based on usage, pretty much + + diff --git a/src/effects.rs b/src/effects.rs new file mode 100644 index 0000000..4c4c110 --- /dev/null +++ b/src/effects.rs @@ -0,0 +1,19 @@ +// Simple types for effects + +use crate::ast::*; + +// bad and wrong and useless +pub struct Effection { + expr: Expression, + effect: Effect, +} + +// yeah i'm not dealing with this yet +pub enum Effect { + Empty, + Total, + Exn, + Pure, + IO, +} + diff --git a/src/main.rs b/src/main.rs new file mode 100644 index 0000000..f31e163 --- /dev/null +++ b/src/main.rs @@ -0,0 +1,51 @@ +use std::io::{Write, stdout, stdin}; +use crate::ast::*; + +mod ast; +mod classes; +mod effects; +mod parser; +mod simple; + +fn main() { + println!("type-systems"); + let mut input = String::new(); + loop { + println!("infer, check, or execute? (i/c/e)"); + print!("\x1b[1m==> \x1b[22m"); + stdout().flush().unwrap(); + + input.clear(); + stdin().read_line(&mut input).unwrap(); + match input.trim() { + "i" | "g" | "infer" => { + println!("enter partially annotated expression to fully infer"); + print!("\x1b[1m====> \x1b[22m"); + stdout().flush().unwrap(); + + input.clear(); + stdin().read_line(&mut input).unwrap(); + simple::infer(Context::new(), parser::parse(&input)); + }, + "c" | "t" | "check" | "typecheck" => { + println!("enter fully annotated expression to typecheck"); + print!("\x1b[1m====> \x1b[22m"); + stdout().flush().unwrap(); + + input.clear(); + stdin().read_line(&mut input).unwrap(); + simple::check(Context::new(), parser::parse(&input)); + }, + "e" | "r" | "execute" | "run" => { + println!("enter expression to execute"); + print!("\x1b[1m====> \x1b[22m"); + stdout().flush().unwrap(); + + input.clear(); + stdin().read_line(&mut input).unwrap(); + simple::execute(Context::new(), parser::parse(&input)); + }, + _ => println!("invalid option {}. please try again.", input.trim()) + } + } +} diff --git a/src/parser.rs b/src/parser.rs new file mode 100644 index 0000000..3223619 --- /dev/null +++ b/src/parser.rs @@ -0,0 +1,6 @@ +use crate::ast::*; + +pub fn parse(input: &str) -> Expression { + let input = input.trim(); + todo!(); +} diff --git a/src/simple.rs b/src/simple.rs new file mode 100644 index 0000000..f71da46 --- /dev/null +++ b/src/simple.rs @@ -0,0 +1,50 @@ +// Simple bidirectional type checking + +use crate::ast::*; + +pub fn infer(context: Context, expression: Expression) { + todo!(); +} + +pub fn check(context: Context, expression: Expression) { + todo!(); +} + +/// Evaluates an expression given a context (of variables) to a term. +/// Panics on non-evaluatable code. +pub fn execute(context: Context, expression: Expression) -> Term { + match expression { + Expression::Annotation { expr, .. } => return execute(context, *expr), + Expression::Constant { term } => return term, + Expression::Variable { id } => return context[&id], + Expression::Abstraction { .. } => panic!(), + Expression::Application { func, arg } => { + match *func { + Expression::Abstraction { param, func } => { + let mut context = context; + context.insert(param, execute(context.clone(), *arg)); + return execute(context, *func); + }, + _ => panic!() + } + }, + Expression::Conditional { if_cond, if_then, if_else } => { + match execute(context.clone(), *if_cond).val { + 1 => execute(context, *if_then), + 0 => execute(context, *if_else), + _ => panic!() + } + }, + } +} + +// intentionally small: i want to run into errors +/// assumption: the count is instantiated to zero +fn uniquify(count: &mut u8) -> String { + *count += 1; + if *count == 0 { + panic!("we've overflowed!"); + } else { + return String::from(format!("{:X}", count)); + } +} |