The problem: In order to prove a specific goal you need all information derivable from a term; and with juggling around only local information, I cannot convince myself I could arrive at a typing system which would prove specific goals given all information derivable in the term.
I am not sure how general this problem actually is. The closest typing system I could look at is Haskell, and there are no results on this problem. I gather they patched a system together which usually works.
The language I am now developing looks naked though. It'll become an experiment in how to write untyped algebraic specifications.
Too slow for anything useful probably but a nice experiment.
After the new language is developed enough, I'll start a new blog. Goodbye Hi.
Hi,
ReplyDeleteWill you post a link to the new blog in this blog?
If so, there will be another last post.
If not, how can we find the new blog?
Hi Ruurd, thank you for your interest.
ReplyDeleteI started a reimplementation of Hi in C++ as an interpreter for various reasons. I got a (Unicode) lexer, parser, and somewhat of a semantics checker finished but failed at getting the type system right.
I am rewriting that project (somewhat slowly at the moment) towards an algebraic specification language aimed at implementing mathematical models.
I will post a github link here once I make the decision to open-source it. I have some dim hopes at creating a product to make some money from it, but that'll likely not pan out.
Thank you again for your interest, I'll make a note to inform you once I've got something to show (publicly).