Last active
January 20, 2022 02:55
-
-
Save jhburns/715bc8009a20b09f554868f35a083667 to your computer and use it in GitHub Desktop.
This file contains hidden or 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
// A minimal reimplementation if mizzle's typechecker in CSharp | |
// https://github.com/jhburns/mizzle/blob/master/src/type_check.rs | |
using System; | |
using System.Collections.Generic; | |
using System.Linq; | |
// Whats the point of this type? | |
// For use in other generic types, like say `Result<Unit, string>` or `Outcome<Unit>` | |
public struct Unit {} | |
// Why use records? Cause C# will auto-implement stuff for us like `==` | |
// These types are declared as records so that equality is automaically implemented for them | |
// Similar to the `Nullable` type | |
public abstract record Option<T> | |
{ | |
public sealed record Some : Option<T> | |
{ | |
public T Data { get; init; } | |
} | |
public sealed record Nil : Option<T> | |
{ | |
} | |
// Convenience funtions | |
public static Option<T> Of(T data) => new Some { Data = data }; | |
} | |
// Like the `Option` type, but a value can also be provided on error | |
public abstract record Result<TOkay, TError> | |
{ | |
public sealed record Okay : Result<TOkay, TError> | |
{ | |
public TOkay Data { get; init; } | |
} | |
public sealed record Error : Result<TOkay, TError> | |
{ | |
public TError Data { get; init; } | |
} | |
// Convenience functions | |
public static Result<TOkay, TError> Ok(TOkay data) => new Okay { Data = data }; | |
public static Result<TOkay, TError> Err(TError data) => new Error { Data = data }; | |
// This function only exists for testing, NOT as an alternative to `switch` | |
public bool IsErr() => this switch | |
{ | |
Result<TOkay, TError>.Okay _ => false, | |
Result<TOkay, TError>.Error _ => true, | |
_ => throw new ArgumentException("Pattern match is not exhaustive"), | |
}; | |
} | |
/** | |
* AST corresponds to this language: | |
* type := "int" | "bool" | |
* | |
* int_literal := regex [0-9] | |
* bool_literal := "true" | "false" | |
* | |
* expression := int_literal | | |
* bool_literal | | |
* expression ":" type | | |
* "if" expression "then" expression "else" expression "end" | |
* | |
* For Example: | |
* ``` | |
* if true : bool then | |
* 3 | |
* else | |
* 4 | |
* end | |
* ``` | |
*/ | |
public enum Type { | |
Bool, | |
Int, | |
} | |
public abstract record Ast { | |
public sealed record IntLiteral : Ast | |
{ | |
public int Data { get; init; } | |
} | |
public sealed record BoolLiteral : Ast | |
{ | |
public bool Data { get; init; } | |
} | |
public sealed record TypeAnnotation : Ast | |
{ | |
public Ast Expression { get; init; } | |
public Type Annotation { get; init; } | |
} | |
public sealed record If : Ast | |
{ | |
public Ast Condition { get; init; } | |
public Ast OnTrue { get; init; } | |
public Ast OnFalse { get; init; } | |
} | |
} | |
// Point of this type is to track errors that may occur | |
// And track the currently infered type | |
public sealed record Outcome<T> { | |
public Option<T> Result { get; init; } | |
public List<string> Errors { get; init; } | |
// Make `Outcome` of a succesful value | |
public static Outcome<T> Of(T data) => new Outcome<T>() { | |
Result = Option<T>.Of(data), | |
Errors = new List<string>(), | |
}; | |
// Make `Outcome` of error value | |
public static Outcome<T> OfErr(string error) => new Outcome<T>() { | |
Result = new Option<T>.Nil(), | |
Errors = new List<string>() { error }, | |
}; | |
// Empty `Outcome` for when needs to be immediatly recovered | |
public static Outcome<Unit> Empty() => new Outcome<Unit> { | |
Result = Option<Unit>.Of(new Unit {}), | |
Errors = new List<string>(), | |
}; | |
// Used for recovering the type checker to continue typechecking | |
// In other words, use this new type but keep the previous errors | |
public Outcome<U> RecoverTo<U>(U item) => new Outcome<U> { | |
Result = Option<U>.Of(item), | |
Errors = Errors, | |
}; | |
// Monadic bind, also known as `bind`, `andThen`, `then`, `let*` and `>>=` | |
// In summary: take an `Outcome` then map over it and flatten | |
public Outcome<U> FlatMap<U>(Func<T, Outcome<U>> flatMapper) { | |
switch (this.Result) { | |
// If the `Outcome` result is something | |
case Option<T>.Some some: { | |
// Then apply the function | |
var nextOutcome = flatMapper(some.Data); | |
return new Outcome<U>() { | |
Result = nextOutcome.Result, | |
// Merge previous errors with new | |
Errors = Errors.Concat(nextOutcome.Errors).ToList(), | |
}; | |
} | |
// If the `Outcome` result is `Nil` do nothing | |
case Option<T>.Nil: | |
return new Outcome<U>() { | |
Result = new Option<U>.Nil(), | |
Errors = Errors, | |
}; | |
default: | |
throw new ArgumentException("Pattern match is not exhaustive"); | |
} | |
} | |
// Monoidal product, also known as `and*` | |
// In summary: take two `Outcome`s, | |
// If they are both successful then return tuple of both values | |
// Otherwise return `Nil` | |
public Outcome<(T, U)> AndZip<U>(Outcome<U> other) { | |
// Merge errors together, first then second | |
var combinedErrors = this.Errors.Concat(other.Errors).ToList(); | |
switch (this.Result, other.Result) { | |
// If Both are `Some`, return a tuple | |
case (Option<T>.Some first, Option<U>.Some second): | |
return new Outcome<(T, U)> { | |
Result = Option<(T, U)>.Of((first.Data, second.Data)), | |
Errors = combinedErrors, | |
}; | |
// If one or more are `Nil`, return `Nil` | |
case (_, _): | |
return new Outcome<(T, U)> { | |
Result = new Option<(T, U)>.Nil(), | |
Errors = combinedErrors, | |
}; | |
default: | |
throw new ArgumentException("Pattern match is not exhaustive"); | |
} | |
} | |
} | |
public sealed class TypeChecker { | |
// Inferes the type of the passes expression | |
private static Outcome<Type> infer(Ast ast) => ast switch | |
{ | |
// Literals have the same type of the literal | |
Ast.IntLiteral lit => Outcome<Type>.Of(Type.Int), | |
Ast.BoolLiteral lit => Outcome<Type>.Of(Type.Bool), | |
// Infer the type of the expression | |
Ast.TypeAnnotation ta => infer(ta.Expression) | |
// If inferring the type was successful, then check if the annotation matches the inferred type | |
// Otherwise no nothing | |
.FlatMap((type) => { | |
if (type == ta.Annotation) | |
{ | |
return Outcome<Unit>.Empty(); | |
} | |
else | |
{ | |
return Outcome<Unit>.OfErr($"Annotation different than expression type: {type} != {ta.Annotation}"); | |
} | |
}) | |
// Recover to the annotated type no matter what | |
.RecoverTo(ta.Annotation), | |
// Infer the type of the `if` condition | |
Ast.If iff => infer(iff.Condition) | |
// If inferring the type was successful, then check that condition is of the type `bool` | |
.FlatMap(type => { | |
if (type == Type.Bool) | |
{ | |
return Outcome<Unit>.Empty(); | |
} | |
else | |
{ | |
return Outcome<Unit>.OfErr($"`if` confiditions have to be a boolean: {type} != bool"); | |
} | |
}) | |
// Recover to `Unit` to guarantee the following happens | |
.RecoverTo(new Unit {}) | |
// Check if both branches of the if are of the same type | |
// `(_)` means we ignore whatever value is being passes, cause its `Unit` in this case | |
.FlatMap((_) => infer(iff.OnTrue).AndZip(infer(iff.OnFalse))) | |
.FlatMap((types) => { | |
if (types.Item1 == types.Item2) | |
{ | |
return Outcome<Type>.Of(types.Item1); | |
} | |
else | |
{ | |
return Outcome<Type>.OfErr($"`if` branches have to be the same type: {types.Item1} != {types.Item2}"); | |
} | |
}), | |
// If they are of different types, don't recover cause it can't be known which one is the "correct" type | |
_ => throw new ArgumentException("Pattern match is not exhaustive"), | |
}; | |
// Wrapper for `infer`, so that it has a safer API | |
public static Result<Type, List<string>> check(Ast ast) { | |
var infered = infer(ast); | |
// If there are any errors, then return only the errors | |
if (infered.Errors.Count() > 0) { | |
return Result<Type, List<string>>.Err(infered.Errors); | |
} else { | |
// This unwraps the `Some`, since we already verfied it should have some value | |
// In other words if there are no errors then an inferred type has to exist | |
// Downcasting is unsafe, and should only be used when its not possible to prove that it is safe using `switch` | |
return Result<Type, List<string>>.Ok(((Option<Type>.Some) infered.Result).Data); | |
} | |
} | |
} | |
public class Program | |
{ | |
// This stuff is all testing | |
static void Assert(bool check) { | |
if (!check) { | |
throw new ArgumentException("Nope"); | |
} | |
} | |
static void Main() | |
{ | |
Assert(TypeChecker.check(new Ast.IntLiteral { Data=1 }) == Result<Type, List<string>>.Ok(Type.Int)); | |
Assert(TypeChecker.check(new Ast.BoolLiteral { Data=true }) == Result<Type, List<string>>.Ok(Type.Bool)); | |
var code0 = new Ast.TypeAnnotation { Expression=new Ast.IntLiteral() { Data = 1 }, Annotation=Type.Int }; | |
Assert(TypeChecker.check(code0) == Result<Type, List<string>>.Ok(Type.Int)); | |
var code1 = new Ast.TypeAnnotation { Expression=new Ast.IntLiteral() { Data=1 }, Annotation=Type.Bool }; | |
Assert(TypeChecker.check(code1).IsErr()); | |
var code2 = new Ast.If { Condition=new Ast.BoolLiteral { Data=true}, OnTrue= new Ast.IntLiteral() { Data=1 }, OnFalse= new Ast.IntLiteral() { Data=2 } }; | |
Assert(TypeChecker.check(code2) == Result<Type, List<string>>.Ok(Type.Int)); | |
var code3 = new Ast.If { Condition=new Ast.BoolLiteral { Data=true}, OnTrue= new Ast.IntLiteral() { Data=1 }, OnFalse= new Ast.BoolLiteral() { Data=false } }; | |
Assert(TypeChecker.check(code3).IsErr()); | |
var code4 = new Ast.If { | |
Condition=new Ast.TypeAnnotation { Expression=new Ast.BoolLiteral { Data=true}, Annotation=Type.Int }, | |
OnTrue= new Ast.IntLiteral() { Data=1 }, | |
OnFalse= new Ast.BoolLiteral() { Data=false } | |
}; | |
var output = (Result<Type, List<string>>.Error) TypeChecker.check(code4); | |
Assert(output.Data.Count() == 3); | |
} | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment