3 ms·

I am currently developing a language, though more as a research project than anything practical. Apologies for jumping on this post, but it is a good opportunit

I am currently developing a language, though more as a research project than anything practical. Apologies for jumping on this post, but it is a good opportunity to organize and set out my thoughts (and possibly someone might find it interesting): Essentially the language is a pure functional language that takes the untyped lambda calculus and adds decoration terms as first class citizens in the calculus. These terms can be used to wrap selected combinators (eg church numerals). The normal beta reduction rules are extended to handle these decorations in a useful way. The decorations allow predicates to be formed that are total over the term space (eg isChurchNumeral?), which means that function call identifiers can be dynamically dispatched based on their arguments (using a certain amount of term assembly from the surface syntax). Adhoc polymorphism can thus be encoded in a transparent fashion. This has been sufficient to build a numerical tower up to and including the Complex numbers, such that the usual operations add, mul, sub, div are defined within and between Natural, Integer, Rational and Complex numbers. It can also manipulate strings as if they were lists, whilst retaining their 'stringyness'. All without needing number or string specific features internal to the runtime (save parsing and formatting on the way in and out). REPL examples: > (sum [1 -3 2.5 3/2 1+2i]) > 3+2i > (reverse "hello") > "olleh" Something resembling Haskell's typeclasses naturally arises, with the usual definitions of Functor, Monad, and Applicative. It is, needless to say, astonishingly slow.

tpush 7y ago
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 building a language, and always interested in seeing novel features like these :).
- 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 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 7y 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.

tpush 7y ago

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 building a language, and always interested in seeing novel features like these :).

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 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 7y 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.