3 ms·
Interesting! Such an extensional definition of a type could be really flexible, but seems like it would be limited to finite types. Is this the case? Or can
by groovy2shoes 10y ago
Interesting! Such an extensional definition of a type could be really flexible, but seems like it would be limited to finite types. Is this the case? Or can you specify types with arbitrary judgments?
- emidln 10y agoIt's only limited in such that you must be able to express the rule using the Shen lisp language. The datatypes are sequents, essentially propositions, that the type checker attempts to prove true. For example, I could define odd integers like this: (datatype odd-integer if (integer? X) if (odd? X) ________________ X : odd-integer;)