Friday, October 16, 2015

Goodbye Hi. Last Post.

So I gave up on implementing a typed language. The problem, in a nutshell, is that I couldn't convince myself I could solve a particular problem associated with constraint typing.

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.