5 ms·

Lolita: A tagless, dependently typed, self-aware programming language

32 points by g0xA52A2A 2y ago

CyberDildonics 2y ago
The name is going to be a problem with anyone taking it seriously but at least the description doesn't make sense.
- leovingi 2y ago
  Thank you for your input on certain names not being taken seriously CyberDildonics
  - CyberDildonics 2y ago
    My 'tagged' CyberDildonics language didn't take off. Maybe I should have made it self-aware.
mchanson 2y ago
The debugger is called Chris Hansen.
- TheCleric 2y ago
  You don’t set breakpoints, you ask a line of code to have a seat over there.
082349872349872 2y ago
It was "Hi World" in blogs. It was "Hello World" on the dotted line. But in my tutorials it was always "Lolita".
tekla 2y ago
[flagged]
- deleted 2y ago
  [deleted]
zeroonetwothree 2y ago
And we wonder why women aren’t especially drawn to programming.
- paxcoder 2y ago
  I am a man, and the name of this language is repulsive to me as well
- Karellen 2y ago
  Especially as, if it were just "In celebration of the 125th anniversary of the birth of Vladimir Nabokov", you'd have thought that something like Pale Fire would be a better choice of name for a tech product. Partly because of all the references to it in Blade Runner 2049, but also because Pale Fire is just a much, much cooler name in general.
  - quickthrowman 2y ago
    Pale Fire has a lot of good names that would work for a programming language. Pale Fire, Kinbote, Shade, Zembla, Waxwing, Gradus …All of which are preferable to the name of the language we are discussing, and I’m saying this as both a fan of the book and film.
    - Karellen 2y ago
      CellsInterlinked
  - 0xfedcafe 2y ago
    Pale Fire sounds awful and lacks any flair. That's exactly what an ordinary programmer with no taste would name their work.
    - lawlessone 2y ago
      >Pale Fire Sounds like name for a craft beer.
  - 2y ago
lawlessone 2y ago
probably could use a different name... jesus.
- Luc 2y ago
  That is possibly even worse!
  - jordanreger 2y ago
    Nah with a good SEO team it'll be the first result on Google
    - 082349872349872 2y ago
      Current Google results: "The Beatles" 105 million Jesus 942 million Sorry, Mr. Lennon.
- slowmovintarget 2y ago
  "The server is risen!"
  - BurdensomeCount 2y ago
    Uptime: Close to 2000 years at this point.
skilled 2y ago
Impressive work. The author looks to be in his very early 20s, and his other blogs talk about compiler development and calculus. The PDF of the language reads like ancient scriptures to me. —— Re: name I have emailed the author about the name choice and whether he would reconsider it as I think this is a high-quality project. The author is on HN (same name as his GH handle) so maybe he will reconsider.
Ekaros 2y ago
What is this tendency of naming so many programming languages with some already relatively common words, why isn't there proper search engine optimization going on? I can kinda excuse pre-internet ones, but new ones? Just why are people making lives hard for others...
- causal 2y ago
  Yup. Even if the authors are totally naive to the negative association, this name renders it simply unusable to many organizations. Simply Googling the name on a work computer could land some people in hot water.
  - dumbo-octopus 2y ago
    It is very likely the case that the author does not particularly care about what happens to people who google the name on their work computers. They are probably firing any customers that expect a dependable system from their hobby project.
- valenterry 2y ago
  Yeah I dislike that too. Very annoying. Not as bad as "go" but still, come on, at least change the name a little bit to make it unique but keep the reference you want to use.
Luc 2y ago
Kind of lives in the same neighborhood as Idris? https://www.idris-lang.org/index.html https://www.idris-lang.org/index.html
GaggiX 2y ago
What would the file extension be?
- deleted 2y ago
  [deleted]
- chriswarbo 2y ago
  The examples use `.lo`
  - BurdensomeCount 2y ago
    She was Lo, plain Lo, in the morning, standing four feet ten in one sock...
puttycat 2y ago
> "In celebration of the 125th anniversary of the birth of Vladimir Nabokov, I am pleased to announce Lolita" So maybe... name it Nabokov?
arolihas 2y ago
I see that the stated reason for the name is that today would have been Nabokov's 125th birthday. But Nabokov had other works (why not call it palefire?) and this could have been released on any particular day. So the connection is tenuous at best. And then there is the docs, taste.md? A taste of Lolita It's a little disturbing.
verbalstone 2y ago
[flagged]
valenterry 2y ago
This is awesome. I love languages like that. It tickles my brain just reading about their metaprogramming attempt.
nomdep 2y ago
Flagged? That's more childish than the name
sbelskie 2y ago
> Couple of inches taller. Pink-rimmed glasses. New, heaped-up hairdo, new ears. How simple! The moment, the death that I had kept conjuring up for three years was as simple as a bit of dry wood. This is on the language FAQ. If memory serves this is the scene where Humbert has tracked down Dolores later in life and is contemplating murdering the now pregnant girl who he earlier sexually abused. What the actual hell? If this is supposed to be a joke it’s in decidedly poor taste. And that’s the best case.
brushfoot 2y ago
At 19, the author's age, I was two years into my Nabokov obsession. I wouldn't have understood why the name was a problem, either. Personally, I'd have thought anyone who criticized it was a philistine. (Nabokov's self-styled "strong opinions" had that effect on me at that age.) Didn't they know the _point_ was that Humbert was a monster, etc. 15 years later, life experience has broadened my horizons a bit, but I still remember the feeling of being under the influence of such an eloquent writer for the first time. This isn't to justify the name itself but to cut the author some slack since the name is attracting more attention here than the design, and understandably so, but the design is an achievement, and a laudable one. I'd hope someone would've done the same for me at that age if I'd gone public with a project like this.
- aebtebeten 2y ago
  Insofar as the pull quotes that don't have plausible deniability are по-русски, I'm pretty sure the author knew what he was doing. (aiming at deliberate* impopularity: широко известный в узких кругах?) That said, https://github.com/lolita-lang/lolita/blob/master/docs/design.md https://github.com/lolita-lang/lolita/blob/master/docs/desig... is impressive, and I guess, as it's open source, someone could always Bowdlerise the project for HN? Don't NAND, don't NAND so Don't NAND so close to me * keep in mind my poor track record: I originally thought the religious conceit of TempleOS might have been a similar ploy.
  - 082349872349872 2y ago
    eg completely SFW, the references for the design doc: Cardelli L. A Polymorphic [lambda]-calculus with Type: Type. – Digital Systems Research Center, 1986. ↩ ↩2 ↩3 John McCarthy. 1960. Recursive functions of symbolic expressions and their computation by machine, Part I. Commun. ACM 3, 4 (April 1960), 184–195. https://doi.org/10.1145/367177.367199 https://doi.org/10.1145/367177.367199 ↩ Turchin, Valentin F.. “A dialogue on Metasystem transition.” World Futures 45 (1995): 5-57. ↩ Jana Dunfield and Neel Krishnaswami. 2021. Bidirectional Typing. ACM Comput. Surv. 54, 5, Article 98 (June 2022), 38 pages. https://doi.org/10.1145/3450952 https://doi.org/10.1145/3450952 ↩ Gundry, Adam and Conor McBride. “A tutorial implementation of dynamic pattern unification A dependently typed programming language implementation pearl.” (2012). ↩ Kovács, András. “Elaboration with first-class implicit function types.” Proceedings of the ACM on Programming Languages 4 (2020): 1 - 29. ↩ Meven Lennon-Bertrand. (2021). Complete Bidirectional Typing for the Calculus of Inductive Constructions. ↩ Luca Cardelli. 1996. Type systems. ACM Comput. Surv. 28, 1 (March 1996), 263–264. https://doi.org/10.1145/234313.234418 https://doi.org/10.1145/234313.234418 ↩ Augustsson, L. (1999). Cayenne — A Language with Dependent Types. In: Swierstra, S.D., Oliveira, J.N., Henriques, P.R. (eds) Advanced Functional Programming. AFP 1998. Lecture Notes in Computer Science, vol 1608. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10704973_6 https://doi.org/10.1007/10704973_6 ↩ ↩2 White, L., Bour, F., & Yallop, J. (2015). Modular implicits. Electronic Proceedings in Theoretical Computer Science, 198, 22–63. ↩ ↩2 Yang, Y., Bi, X., Oliveira, B.C.d.S. (2016). Unified Syntax with Iso-types. In: Igarashi, A. (eds) Programming Languages and Systems. APLAS 2016. Lecture Notes in Computer Science(), vol 10017. Springer, Cham. https://doi.org/10.1007/978-3-319-47958-3_14 https://doi.org/10.1007/978-3-319-47958-3_14 ↩ ↩2 ↩3 Yang, Y., Bi, X., Oliveira, B.C.d.S.: Unified syntax with iso-types. Extended ver- sion available from https://bitbucket.org/ypyang/aplas16 https://bitbucket.org/ypyang/aplas16 (2016) ↩ Adam Chlipala. 2008. Parametric higher-order abstract syntax for mechanized semantics. In Proceedings of the 13th ACM SIGPLAN international conference on Functional programming (ICFP '08). Association for Computing Machinery, New York, NY, USA, 143–156. https://doi.org/10.1145/1411204.1411226 https://doi.org/10.1145/1411204.1411226 ↩ Gibbons, Jeremy & Wu, Nicolas. (2014). Folding domain-specific languages: Deep and shallow embeddings (functional Pearl). Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP. 49. 10.1145/2628136.2628138. ↩ Carette, J., Kiselyov, O., Shan, Cc. (2007). Finally Tagless, Partially Evaluated. In: Shao, Z. (eds) Programming Languages and Systems. APLAS 2007. Lecture Notes in Computer Science, vol 4807. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-76637-7_15 https://doi.org/10.1007/978-3-540-76637-7_15 ↩ ↩2 ↩3 ↩4 Kiselyov, O. (2012). Typed Tagless Final Interpreters. In: Gibbons, J. (eds) Generic and Indexed Programming. Lecture Notes in Computer Science, vol 7470. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32202-0_3 https://doi.org/10.1007/978-3-642-32202-0_3 ↩ ↩2 Coquand, Thierry & Kinoshita, Yoshiki & Nordstrom, Bengt & Takeyama, Makoto. (2009). A simple type-theoretic language: Mini-TT. From Semantics to Computer Science: Essays in Honour of Gilles Kahn. 10.1017/CBO9780511770524.007. ↩ ↩2 Altenkirch, T., Danielsson, N.A., Löh, A., Oury, N. (2010). ΠΣ: Dependent Types without the Sugar. In: Blume, M., Kobayashi, N., Vidal, G. (eds) Functional and Logic Programming. FLOPS 2010. Lecture Notes in Computer Science, vol 6009. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12251-4_5 https://doi.org/10.1007/978-3-642-12251-4_5 ↩ Fu, P., Stump, A. (2014). Self Types for Dependently Typed Lambda Encodings. In: Dowek, G. (eds) Rewriting and Typed Lambda Calculi. RTA TLCA 2014 2014. Lecture Notes in Computer Science, vol 8560. Springer, Cham. https://doi.org/10.1007/978-3-319-08918-8_16 https://doi.org/10.1007/978-3-319-08918-8_16 ↩ KISELYOV O, MU S-C, SABRY A. Not by equations alone: Reasoning with extensible effects. Journal of Functional Programming. 2021;31:e2. doi:10.1017/S0956796820000271 ↩ Wadler, P. (1993). Monads for functional programming. In: Broy, M. (eds) Program Design Calculi. NATO ASI Series, vol 118. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-02880-3_8 https://doi.org/10.1007/978-3-662-02880-3_8 ↩ Pretnar, Matija. (2015). An Introduction to Algebraic Effects and Handlers. Invited tutorial paper. Electronic Notes in Theoretical Computer Science. 319. 19-35. 10.1016/j.entcs.2015.12.003. ↩ P. Wadler and S. Blott. 1989. How to make ad-hoc polymorphism less ad hoc. In Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '89). Association for Computing Machinery, New York, NY, USA, 60–76. https://doi.org/10.1145/75277.75283 https://doi.org/10.1145/75277.75283 ↩ Meijer, E., Hughes, J. (Ed.), Fokkinga, M. M., & Paterson, R. (1991). Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. 124-144. Paper presented at 5th ACM Conference on Functional Programming Languages and Computer Architecture (FPCA 1991). https://doi.org/10.1007/3540543961_7 https://doi.org/10.1007/3540543961_7 ↩ Peyton Jones, Simon. (2002). Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. ↩ Turchin V., Nemytykh, A. Metavariables: Their implementation and use in Program Transformation, CCNY Technical Report CSc TR-95-012, 1995. ↩ ↩2 Turchin V., Refal-5, Programming Guide and Reference Manual, New England Publishing Co., 1989. ↩ Nemytykh, A.P., Pinchuk, V.A., Turchin, V.F. (1996). A Self-Applicable supercompiler. In: Danvy, O., Glück, R., Thiemann, P. (eds) Partial Evaluation. Lecture Notes in Computer Science, vol 1110. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61580-6_16 https://doi.org/10.1007/3-540-61580-6_16 ↩ Turchin, Valentin F.. “Program transformation with metasystem transitions.” Journal of Functional Programming 3 (1993): 283 - 313. ↩ Robert Glück and Morten Heine Sørensen. 1996. A Roadmap to Metacomputation by Supercompilation. In Selected Papers from the International Seminar on Partial Evaluation. Springer-Verlag, Berlin, Heidelberg, 137–160. ↩ Futamura, Y. (1983). Partial computation of programs. In: Goto, E., Furukawa, K., Nakajima, R., Nakata, I., Yonezawa, A. (eds) RIMS Symposia on Software Science and Engineering. Lecture Notes in Computer Science, vol 147. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-11980-9_13 https://doi.org/10.1007/3-540-11980-9_13 ↩ A.V. Klimov and S.A. Romanenko. Metavychislitel' dlja jazyka Refal. Osnovnye ponjatija i primery. (A metaevaluator for the language Refal. Basic concepts and examples). Preprint 71, Keldysh Institute of Applied Mathematics, Academy of Sciences of the USSR, Moscow, 1987. ↩ John Lamping. 1989. An algorithm for optimal lambda calculus reduction. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '90). Association for Computing Machinery, New York, NY, USA, 16–30. https://doi.org/10.1145/96709.96711 https://doi.org/10.1145/96709.96711 ↩ Yves Lafont. 1989. Interaction nets. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '90). Association for Computing Machinery, New York, NY, USA, 95–108. https://doi.org/10.1145/96709.96718 https://doi.org/10.1145/96709.96718 ↩ Yves Lafont. 1997. Interaction Combinators. Inf. Comput. 137, 1 (Aug. 25, 1997), 69–101. https://doi.org/10.1006/inco.1997.2643 https://doi.org/10.1006/inco.1997.2643 ↩ Andrea Asperti. (2017). About the efficient reduction of lambda terms. ↩ Cas van der Rest, Jaro Reinders, & Casper Bach Poulsen. (2022). Handling Higher-Order Effects. ↩ Thierry Coquand, & Gérard Huet (1988). The calculus of constructions. Information and Computation, 76(2), 95-120. ↩ 1948, Human Knowledge: Its Scope and Limits by Bertrand Russell, Section: Part II: Language, Chapter I: The Uses of Language Quote Page 60, Simon and Schuster, New York. ↩ Turchin, Valentin F. "Equivalent transformations of Refal programs." Avtomatizirovannaja Sistema upravlenija stroitel'stvom. Trudy CNIPIASS 6 (1974): 36-68. ↩ Dijkstra, Edsger W.. “A Discipline of Programming.” (1976). ↩ Perlis, Alan J.. “Epigrams on Programming.” Sigplan Notices 17 (1982): 7-13. ↩ Edsger W. Dijkstra. 1972. The humble programmer. Commun. ACM 15, 10 (Oct. 1972), 859–866. https://doi.org/10.1145/355604.361591 https://doi.org/10.1145/355604.361591 ↩
ilaksh 2y ago
Anyone care to do a direct comparison with Ocaml? It seems that the types are featured more prominently here. I always thought that type inference was a strength of Ocaml. Maybe that is unpopular now?
- chriswarbo 2y ago
  Ocaml, being in the ML family, makes heavy use of Algebraic Datatypes. For example, from https://www.ocaml.org/manual/5.1/api/List.html https://www.ocaml.org/manual/5.1/api/List.html we can encode lists like this: type 'a t = 'a list = | [] | (::) of 'a * 'a list In other words, values of type `'a list` are either `[]` (the empty list, like `nil` in Lisp), or `(::)` applied to two arguments (prepending an element to a list, like `cons` in Lisp). We can tell whether a particular value is one of the other by storing a bit of information, called a "tag". We can later branch on that bit to perform pattern-matching. In constrast, the "tagless" encoding seems closer to Church-encoding. A Church-encoded list is a function which accepts two arguments, say `x` and `y`: - An "empty list" will return `x` as-is. - A non-empty list will call `y` with two arguments: one argument is the first element of the list, and the other argument is the result of calling the tail of the list with `x` and `y`. Such functions have many other names, like "elimination forms", or "induction/recursion schemes", etc. The linked page shows an example of implementing lists using the tagless approach, which like Church encoding but collects together the required parts in a record. I reckon a similar approach could be implemented via modules, but am not too experienced in Ocaml to know how easy/awkward that would be.
joemi 2y ago
What makes it "self-aware"? That was the main reason I clicked on the link but I didn't see that explained.
- chriswarbo 2y ago
  Presumably the way macros are implemented, using a partially-evaluated metacircular-interpreter.
chriswarbo 2y ago
Very impressive feature set, which aligns with many of my own interests too (symbolic execution, partial evaluation, etc.). If nothing else, it's the first explanation of "finally tagless" that clicked for me! I agree with others that the name is needlessly off-putting.
fuki 2y ago
Could use a different name
xigoi 2y ago
It seems to have been taken down, presumably because of the name. Does anyone know if it’s available under a digferent name now?

32 points by g0xA52A2A 2y ago

CyberDildonics 2y ago

The name is going to be a problem with anyone taking it seriously but at least the description doesn't make sense.

leovingi 2y ago
Thank you for your input on certain names not being taken seriously CyberDildonics
- CyberDildonics 2y ago
  My 'tagged' CyberDildonics language didn't take off. Maybe I should have made it self-aware.

mchanson 2y ago

The debugger is called Chris Hansen.

TheCleric 2y ago
You don’t set breakpoints, you ask a line of code to have a seat over there.

082349872349872 2y ago

It was "Hi World" in blogs. It was "Hello World" on the dotted line. But in my tutorials it was always "Lolita".

tekla 2y ago

[flagged]

deleted 2y ago
[deleted]

zeroonetwothree 2y ago

And we wonder why women aren’t especially drawn to programming.

paxcoder 2y ago
I am a man, and the name of this language is repulsive to me as well
Karellen 2y ago
Especially as, if it were just "In celebration of the 125th anniversary of the birth of Vladimir Nabokov", you'd have thought that something like Pale Fire would be a better choice of name for a tech product. Partly because of all the references to it in Blade Runner 2049, but also because Pale Fire is just a much, much cooler name in general.
- quickthrowman 2y ago
  Pale Fire has a lot of good names that would work for a programming language. Pale Fire, Kinbote, Shade, Zembla, Waxwing, Gradus …All of which are preferable to the name of the language we are discussing, and I’m saying this as both a fan of the book and film.
  - Karellen 2y ago
    CellsInterlinked
- 0xfedcafe 2y ago
  Pale Fire sounds awful and lacks any flair. That's exactly what an ordinary programmer with no taste would name their work.
  - lawlessone 2y ago
    >Pale Fire Sounds like name for a craft beer.
- 2y ago

lawlessone 2y ago

probably could use a different name... jesus.

Luc 2y ago
That is possibly even worse!
- jordanreger 2y ago
  Nah with a good SEO team it'll be the first result on Google
  - 082349872349872 2y ago
    Current Google results: "The Beatles" 105 million Jesus 942 million Sorry, Mr. Lennon.
slowmovintarget 2y ago
"The server is risen!"
- BurdensomeCount 2y ago
  Uptime: Close to 2000 years at this point.

skilled 2y ago

Impressive work. The author looks to be in his very early 20s, and his other blogs talk about compiler development and calculus. The PDF of the language reads like ancient scriptures to me. —— Re: name I have emailed the author about the name choice and whether he would reconsider it as I think this is a high-quality project. The author is on HN (same name as his GH handle) so maybe he will reconsider.

Ekaros 2y ago

What is this tendency of naming so many programming languages with some already relatively common words, why isn't there proper search engine optimization going on? I can kinda excuse pre-internet ones, but new ones? Just why are people making lives hard for others...

causal 2y ago
Yup. Even if the authors are totally naive to the negative association, this name renders it simply unusable to many organizations. Simply Googling the name on a work computer could land some people in hot water.
- dumbo-octopus 2y ago
  It is very likely the case that the author does not particularly care about what happens to people who google the name on their work computers. They are probably firing any customers that expect a dependable system from their hobby project.
valenterry 2y ago
Yeah I dislike that too. Very annoying. Not as bad as "go" but still, come on, at least change the name a little bit to make it unique but keep the reference you want to use.

Luc 2y ago

Kind of lives in the same neighborhood as Idris? https://www.idris-lang.org/index.html https://www.idris-lang.org/index.html

GaggiX 2y ago

What would the file extension be?

deleted 2y ago
[deleted]
chriswarbo 2y ago
The examples use `.lo`
- BurdensomeCount 2y ago
  She was Lo, plain Lo, in the morning, standing four feet ten in one sock...

puttycat 2y ago

> "In celebration of the 125th anniversary of the birth of Vladimir Nabokov, I am pleased to announce Lolita" So maybe... name it Nabokov?

arolihas 2y ago

I see that the stated reason for the name is that today would have been Nabokov's 125th birthday. But Nabokov had other works (why not call it palefire?) and this could have been released on any particular day. So the connection is tenuous at best. And then there is the docs, taste.md? A taste of Lolita It's a little disturbing.

verbalstone 2y ago

[flagged]

valenterry 2y ago

This is awesome. I love languages like that. It tickles my brain just reading about their metaprogramming attempt.

nomdep 2y ago

Flagged? That's more childish than the name

sbelskie 2y ago

> Couple of inches taller. Pink-rimmed glasses. New, heaped-up hairdo, new ears. How simple! The moment, the death that I had kept conjuring up for three years was as simple as a bit of dry wood. This is on the language FAQ. If memory serves this is the scene where Humbert has tracked down Dolores later in life and is contemplating murdering the now pregnant girl who he earlier sexually abused. What the actual hell? If this is supposed to be a joke it’s in decidedly poor taste. And that’s the best case.

brushfoot 2y ago

At 19, the author's age, I was two years into my Nabokov obsession. I wouldn't have understood why the name was a problem, either. Personally, I'd have thought anyone who criticized it was a philistine. (Nabokov's self-styled "strong opinions" had that effect on me at that age.) Didn't they know the _point_ was that Humbert was a monster, etc. 15 years later, life experience has broadened my horizons a bit, but I still remember the feeling of being under the influence of such an eloquent writer for the first time. This isn't to justify the name itself but to cut the author some slack since the name is attracting more attention here than the design, and understandably so, but the design is an achievement, and a laudable one. I'd hope someone would've done the same for me at that age if I'd gone public with a project like this.

aebtebeten 2y ago
Insofar as the pull quotes that don't have plausible deniability are по-русски, I'm pretty sure the author knew what he was doing. (aiming at deliberate* impopularity: широко известный в узких кругах?) That said, https://github.com/lolita-lang/lolita/blob/master/docs/design.md https://github.com/lolita-lang/lolita/blob/master/docs/desig... is impressive, and I guess, as it's open source, someone could always Bowdlerise the project for HN? Don't NAND, don't NAND so Don't NAND so close to me * keep in mind my poor track record: I originally thought the religious conceit of TempleOS might have been a similar ploy.
- 082349872349872 2y ago
  eg completely SFW, the references for the design doc: Cardelli L. A Polymorphic [lambda]-calculus with Type: Type. – Digital Systems Research Center, 1986. ↩ ↩2 ↩3 John McCarthy. 1960. Recursive functions of symbolic expressions and their computation by machine, Part I. Commun. ACM 3, 4 (April 1960), 184–195. https://doi.org/10.1145/367177.367199 https://doi.org/10.1145/367177.367199 ↩ Turchin, Valentin F.. “A dialogue on Metasystem transition.” World Futures 45 (1995): 5-57. ↩ Jana Dunfield and Neel Krishnaswami. 2021. Bidirectional Typing. ACM Comput. Surv. 54, 5, Article 98 (June 2022), 38 pages. https://doi.org/10.1145/3450952 https://doi.org/10.1145/3450952 ↩ Gundry, Adam and Conor McBride. “A tutorial implementation of dynamic pattern unification A dependently typed programming language implementation pearl.” (2012). ↩ Kovács, András. “Elaboration with first-class implicit function types.” Proceedings of the ACM on Programming Languages 4 (2020): 1 - 29. ↩ Meven Lennon-Bertrand. (2021). Complete Bidirectional Typing for the Calculus of Inductive Constructions. ↩ Luca Cardelli. 1996. Type systems. ACM Comput. Surv. 28, 1 (March 1996), 263–264. https://doi.org/10.1145/234313.234418 https://doi.org/10.1145/234313.234418 ↩ Augustsson, L. (1999). Cayenne — A Language with Dependent Types. In: Swierstra, S.D., Oliveira, J.N., Henriques, P.R. (eds) Advanced Functional Programming. AFP 1998. Lecture Notes in Computer Science, vol 1608. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10704973_6 https://doi.org/10.1007/10704973_6 ↩ ↩2 White, L., Bour, F., & Yallop, J. (2015). Modular implicits. Electronic Proceedings in Theoretical Computer Science, 198, 22–63. ↩ ↩2 Yang, Y., Bi, X., Oliveira, B.C.d.S. (2016). Unified Syntax with Iso-types. In: Igarashi, A. (eds) Programming Languages and Systems. APLAS 2016. Lecture Notes in Computer Science(), vol 10017. Springer, Cham. https://doi.org/10.1007/978-3-319-47958-3_14 https://doi.org/10.1007/978-3-319-47958-3_14 ↩ ↩2 ↩3 Yang, Y., Bi, X., Oliveira, B.C.d.S.: Unified syntax with iso-types. Extended ver- sion available from https://bitbucket.org/ypyang/aplas16 https://bitbucket.org/ypyang/aplas16 (2016) ↩ Adam Chlipala. 2008. Parametric higher-order abstract syntax for mechanized semantics. In Proceedings of the 13th ACM SIGPLAN international conference on Functional programming (ICFP '08). Association for Computing Machinery, New York, NY, USA, 143–156. https://doi.org/10.1145/1411204.1411226 https://doi.org/10.1145/1411204.1411226 ↩ Gibbons, Jeremy & Wu, Nicolas. (2014). Folding domain-specific languages: Deep and shallow embeddings (functional Pearl). Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP. 49. 10.1145/2628136.2628138. ↩ Carette, J., Kiselyov, O., Shan, Cc. (2007). Finally Tagless, Partially Evaluated. In: Shao, Z. (eds) Programming Languages and Systems. APLAS 2007. Lecture Notes in Computer Science, vol 4807. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-76637-7_15 https://doi.org/10.1007/978-3-540-76637-7_15 ↩ ↩2 ↩3 ↩4 Kiselyov, O. (2012). Typed Tagless Final Interpreters. In: Gibbons, J. (eds) Generic and Indexed Programming. Lecture Notes in Computer Science, vol 7470. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32202-0_3 https://doi.org/10.1007/978-3-642-32202-0_3 ↩ ↩2 Coquand, Thierry & Kinoshita, Yoshiki & Nordstrom, Bengt & Takeyama, Makoto. (2009). A simple type-theoretic language: Mini-TT. From Semantics to Computer Science: Essays in Honour of Gilles Kahn. 10.1017/CBO9780511770524.007. ↩ ↩2 Altenkirch, T., Danielsson, N.A., Löh, A., Oury, N. (2010). ΠΣ: Dependent Types without the Sugar. In: Blume, M., Kobayashi, N., Vidal, G. (eds) Functional and Logic Programming. FLOPS 2010. Lecture Notes in Computer Science, vol 6009. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12251-4_5 https://doi.org/10.1007/978-3-642-12251-4_5 ↩ Fu, P., Stump, A. (2014). Self Types for Dependently Typed Lambda Encodings. In: Dowek, G. (eds) Rewriting and Typed Lambda Calculi. RTA TLCA 2014 2014. Lecture Notes in Computer Science, vol 8560. Springer, Cham. https://doi.org/10.1007/978-3-319-08918-8_16 https://doi.org/10.1007/978-3-319-08918-8_16 ↩ KISELYOV O, MU S-C, SABRY A. Not by equations alone: Reasoning with extensible effects. Journal of Functional Programming. 2021;31:e2. doi:10.1017/S0956796820000271 ↩ Wadler, P. (1993). Monads for functional programming. In: Broy, M. (eds) Program Design Calculi. NATO ASI Series, vol 118. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-02880-3_8 https://doi.org/10.1007/978-3-662-02880-3_8 ↩ Pretnar, Matija. (2015). An Introduction to Algebraic Effects and Handlers. Invited tutorial paper. Electronic Notes in Theoretical Computer Science. 319. 19-35. 10.1016/j.entcs.2015.12.003. ↩ P. Wadler and S. Blott. 1989. How to make ad-hoc polymorphism less ad hoc. In Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '89). Association for Computing Machinery, New York, NY, USA, 60–76. https://doi.org/10.1145/75277.75283 https://doi.org/10.1145/75277.75283 ↩ Meijer, E., Hughes, J. (Ed.), Fokkinga, M. M., & Paterson, R. (1991). Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. 124-144. Paper presented at 5th ACM Conference on Functional Programming Languages and Computer Architecture (FPCA 1991). https://doi.org/10.1007/3540543961_7 https://doi.org/10.1007/3540543961_7 ↩ Peyton Jones, Simon. (2002). Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. ↩ Turchin V., Nemytykh, A. Metavariables: Their implementation and use in Program Transformation, CCNY Technical Report CSc TR-95-012, 1995. ↩ ↩2 Turchin V., Refal-5, Programming Guide and Reference Manual, New England Publishing Co., 1989. ↩ Nemytykh, A.P., Pinchuk, V.A., Turchin, V.F. (1996). A Self-Applicable supercompiler. In: Danvy, O., Glück, R., Thiemann, P. (eds) Partial Evaluation. Lecture Notes in Computer Science, vol 1110. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61580-6_16 https://doi.org/10.1007/3-540-61580-6_16 ↩ Turchin, Valentin F.. “Program transformation with metasystem transitions.” Journal of Functional Programming 3 (1993): 283 - 313. ↩ Robert Glück and Morten Heine Sørensen. 1996. A Roadmap to Metacomputation by Supercompilation. In Selected Papers from the International Seminar on Partial Evaluation. Springer-Verlag, Berlin, Heidelberg, 137–160. ↩ Futamura, Y. (1983). Partial computation of programs. In: Goto, E., Furukawa, K., Nakajima, R., Nakata, I., Yonezawa, A. (eds) RIMS Symposia on Software Science and Engineering. Lecture Notes in Computer Science, vol 147. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-11980-9_13 https://doi.org/10.1007/3-540-11980-9_13 ↩ A.V. Klimov and S.A. Romanenko. Metavychislitel' dlja jazyka Refal. Osnovnye ponjatija i primery. (A metaevaluator for the language Refal. Basic concepts and examples). Preprint 71, Keldysh Institute of Applied Mathematics, Academy of Sciences of the USSR, Moscow, 1987. ↩ John Lamping. 1989. An algorithm for optimal lambda calculus reduction. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '90). Association for Computing Machinery, New York, NY, USA, 16–30. https://doi.org/10.1145/96709.96711 https://doi.org/10.1145/96709.96711 ↩ Yves Lafont. 1989. Interaction nets. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '90). Association for Computing Machinery, New York, NY, USA, 95–108. https://doi.org/10.1145/96709.96718 https://doi.org/10.1145/96709.96718 ↩ Yves Lafont. 1997. Interaction Combinators. Inf. Comput. 137, 1 (Aug. 25, 1997), 69–101. https://doi.org/10.1006/inco.1997.2643 https://doi.org/10.1006/inco.1997.2643 ↩ Andrea Asperti. (2017). About the efficient reduction of lambda terms. ↩ Cas van der Rest, Jaro Reinders, & Casper Bach Poulsen. (2022). Handling Higher-Order Effects. ↩ Thierry Coquand, & Gérard Huet (1988). The calculus of constructions. Information and Computation, 76(2), 95-120. ↩ 1948, Human Knowledge: Its Scope and Limits by Bertrand Russell, Section: Part II: Language, Chapter I: The Uses of Language Quote Page 60, Simon and Schuster, New York. ↩ Turchin, Valentin F. "Equivalent transformations of Refal programs." Avtomatizirovannaja Sistema upravlenija stroitel'stvom. Trudy CNIPIASS 6 (1974): 36-68. ↩ Dijkstra, Edsger W.. “A Discipline of Programming.” (1976). ↩ Perlis, Alan J.. “Epigrams on Programming.” Sigplan Notices 17 (1982): 7-13. ↩ Edsger W. Dijkstra. 1972. The humble programmer. Commun. ACM 15, 10 (Oct. 1972), 859–866. https://doi.org/10.1145/355604.361591 https://doi.org/10.1145/355604.361591 ↩

ilaksh 2y ago

Anyone care to do a direct comparison with Ocaml? It seems that the types are featured more prominently here. I always thought that type inference was a strength of Ocaml. Maybe that is unpopular now?

chriswarbo 2y ago
Ocaml, being in the ML family, makes heavy use of Algebraic Datatypes. For example, from https://www.ocaml.org/manual/5.1/api/List.html https://www.ocaml.org/manual/5.1/api/List.html we can encode lists like this: type 'a t = 'a list = | [] | (::) of 'a * 'a list In other words, values of type `'a list` are either `[]` (the empty list, like `nil` in Lisp), or `(::)` applied to two arguments (prepending an element to a list, like `cons` in Lisp). We can tell whether a particular value is one of the other by storing a bit of information, called a "tag". We can later branch on that bit to perform pattern-matching. In constrast, the "tagless" encoding seems closer to Church-encoding. A Church-encoded list is a function which accepts two arguments, say `x` and `y`: - An "empty list" will return `x` as-is. - A non-empty list will call `y` with two arguments: one argument is the first element of the list, and the other argument is the result of calling the tail of the list with `x` and `y`. Such functions have many other names, like "elimination forms", or "induction/recursion schemes", etc. The linked page shows an example of implementing lists using the tagless approach, which like Church encoding but collects together the required parts in a record. I reckon a similar approach could be implemented via modules, but am not too experienced in Ocaml to know how easy/awkward that would be.

joemi 2y ago

What makes it "self-aware"? That was the main reason I clicked on the link but I didn't see that explained.

chriswarbo 2y ago
Presumably the way macros are implemented, using a partially-evaluated metacircular-interpreter.

chriswarbo 2y ago

Very impressive feature set, which aligns with many of my own interests too (symbolic execution, partial evaluation, etc.). If nothing else, it's the first explanation of "finally tagless" that clicked for me! I agree with others that the name is needlessly off-putting.

fuki 2y ago

Could use a different name

xigoi 2y ago

It seems to have been taken down, presumably because of the name. Does anyone know if it’s available under a digferent name now?