4 ms·
Possibly an alternative - but operating at the term level as predicates - if you consider 'type' to be a total function dividing your term space into 'of the ty
by somewhereoutth 7y ago
Possibly an alternative - but operating at the term level as predicates - if you consider 'type' to be a total function dividing your term space into 'of the type' and 'not of the type'.
Church numerals:
0 = (^Nat (\f \x x))
1 = (^Nat (\f \x (f x)))
The ^Nat is the decoration, and can be recovered with a special predicate function ?Nat. So:
(?Nat (^Nat (\f \x x))) =>Beta (^Bool (\x \y x)) *i.e. true*
For this to work the inner part must be reduced first. It does seem to be consistent with Normal order reduction - the Y combinator etc work as expected.
- abecedarius 7y agoIt sounds like the trademarks in https://blog.acolyer.org/2016/10/19/protection-in-programming-languages/ https://blog.acolyer.org/2016/10/19/protection-in-programmin... -- is that right?
- somewhereoutth 7y agoKind of - but more about dynamic dispatch / overloaded function name resolution than protection per se. Furthermore, the decorations work at the lowest possible level, and are bound up with the extended beta reduction (there is also an unwrap operator with associated reduction rules). Of course, any computation can be modelled in the standard lambda calculus, without needing to hack the reduction, but I believe that this extension is in some sense non-trivial as it would require the LC to first implement the LC terms and usual beta reduction within itself, before then implementing the additional terms and redux.