3 ms·
In Shen, we easily typecheck foo to the specific values 42 and "forty-two", not merely either String or Int. \\ enforce type checking (tc +) \\ cr
by emidln 10y ago
In Shen, we easily typecheck foo to the specific values 42 and "forty-two", not merely either String or Int.
\\ enforce type checking
(tc +)
\\ create a forty-two type
(datatype forty-two
_______________
42 : forty-two;
________________________
"forty-two" : forty-two;)
\* example
(7+) 42
42 : number
(8+) 42 : number
42 : forty-two
(9+) 43
43 : number
(10+) 43 : forty-two
type error
*\
\\ define our foo that takes a boolean
\\ value and returns a forty-two
(define foo
{ boolean --> forty-two }
X -> (if X 42 "forty-two"))
\* example
(4+) (== (forty-two true) 42)
true : boolean
(5+) (== (forty-two false) "forty-two")
true : boolean
*\
- groovy2shoes 10y agoInteresting! 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;)