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!
0 Boosts
0 Likes
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.
