OSDN Git Service

Proper types, checking, inference.
authorSimon Forman <sforman@hushmail.com>
Sun, 26 Jan 2020 16:43:52 +0000 (08:43 -0800)
committerSimon Forman <sforman@hushmail.com>
Sun, 26 Jan 2020 16:43:52 +0000 (08:43 -0800)
commit2aa1765b897f4b7ad50ce783d35f58afbde67b64
treec1110fe3ee4e01ab7f76b3181d8ee7fdc55c9c9a
parent6e6e52d206c7365bc579eab069ae9779c5e3f2b5
Proper types, checking, inference.

When I first translated Joy into Prolog I was so blown away by the Prolog
unification over list structures and Triska's CLP(FD) semantics for math
(both in the sense that he wrote CLP(FD) for SWI Prolog and he suggested
it for Joy-in-Prolog specifically) that I didn't realize that it wasn't
quite type inference.

It's kind of like type inference, in that lists are handled correctly and
the CLP(FD) library creates and maintains a kind of context for
constraints, which are sort-of like "dependent types" if you squint a
little.  But you can still do things like 'cons' a number to a number and
get (a Prolog term) like [2|3] which is almost certainly a bug.

So I went through and added type "tags" as Prolog terms: int/1, list/1,
and symbol/1.  The parser assigns them and all the primitive functions
and combinators use them (and so all the definitions do too.)  With this
information Prolog can e.g. prevent attempts to add numbers and lists, and
so on.

This also allows for the thun/3 relation to be implemented a little more
efficiently (without much loss of beauty) by looking ahead one term in
the pending expression and dispatching on structural "type" in a thun/4
relation.  I miss the elegance of the previous version, but this lets
Prolog index on the structural type tags that the parser produces.

(This might mess up tail recursion because now we have a loop between
thun/3 and thun/4 but we can eliminate that problem by partial reduction
on thun/3.  TODO.)

Now that literals are tagged by the parser there's no need for literal/1.
thun/thun.pl