Logic subsystem

[mikera]

Consider a core.logic style system for Magic

Considerations:

• This might be very useful (essential?) for good type inference
• Could be useful to define Relation types as part of the core language

[arrdem]

So Shen is super interesting (despite its other various insanities) because it uses a language level implementation of prolog to do arbitrary constraint search / proof for typechecking. The runtime itself is functionally untyped being a mu lisp, with all the type checking being done entirely as the user opts into it at the language level.

[mikera]

Thanks that is interesting - I had a quick look at Shen but it seems very academic. I don't want to require users to be experts in type theory to be able to create a working well-typed program!

But it is good to know that a language level logic system is a feasible way to approach this, I will take a look at how they implement this.