4 ms·

From your description it sounds like these decorators are an alternative to type annotations? Mind showing how these decorators look and work? I'm also buildin

• somewhereoutth 6y 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 6y ago
    It 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 6y ago
      Kind 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.