Alonzo research news: Reading up on Algorithm W didn't really the questions I had. Now I'm studying up on System Fω, at 1st glance this looks like a close fit...
I'm trying to figure out how to implement a typechecker!
1 Boost
0 Likes
@theruran @jonmsterling Thanks, I will!
@alcinnz @theruran A great resource to check out is the Elaboration Zoo by @AndrasKovacs : https://github.com/AndrasKovacs/elaboration-zoo/.
This federated comment is not yet available here.
@wizzwizz4 @bkim Thanks for your faith in me!
System Fω really seems like it... Semantically Alonzo's barely any different!
@alcinnz I've started trying to write a typechecker, then read that it's the same unification used by Prolog, then tried to implement a Prolog, and now I'm on year 6 of studying programming languages and haven't finished writing typecheckers.
@bkim Yeah its harder than I thought...
But hopefully I want spend that much time!
@alcinnz if you want a reference unification algorithm to study from, this is my toy Prolog implementation: https://github.com/brunokim/prol/blob/main/interpreter.py#L672
The mapping to algorithm W would be
Atom -> type literal, e.g., int, str, etc.
Ref -> unbound type
Struct/functor -> complex type, like a function type with arg types and return type.
@alcinnz it's not that it's inherently difficult, but often powerful and with subtle consequences. And after you write a part of the toy language, you want to also add some syntactic sugar, and classes, and debugging facilities, and a faster parser, and...
What I'm trying to do now is MVP-ing my newest language, where I
1) write the code that I want
2) implement the bare minimum to run it
The code is in a single file and riddled with `raise NotImplementedError`, but I'm having a lot of fun!
@alcinnz check out @jonmsterling 's seminar on this topic!
https://www.jonmsterling.com/sterling-2022-hottest-colloqium/
How to code your own type theory