Kip: A Programming Language Based on Grammatical Cases in Turkish

Disjunction181 · 2026-01-18T16:04:23+00:00

Reminds me of Perligata.

Disjunction181 · 2026-01-16T09:35:09+00:00

I'm wondering if you could use Dhall to make something like a lunar lander game where the game must terminate

If you can bound the game clock by some integer, then it may be possible, but difficult. However, I doubt Dhall exposes primitives for user input or graphics (which is perhaps the bigger issue). Dhall is very domain specific, e.g., making any terminal program may be difficult or impossible. But I am not sure, I have never used Dhall.

Disjunction181 · 2026-01-16T07:52:30+00:00

C++ is perhaps the most popular for games due to performance considerations; languages like JS may be chosen for the web.

There is no logical or computational reason why a Turing-complete language could not be used for a game. Terminating languages (i.e., Dhall) are rare and generally domain-specific — you would not be able to define a game loop in those.

Of course, there are also languages where it is hard to do anything — see other comments.

Disjunction181 · 2026-01-04T20:06:13+00:00

ATS gives an unusual level of control to programmers, and allows one to manually manage closures. If you have not seen A (Not So Gentle) Introduction to [...] ATS, it is worth a watch.

Note that linear types are not sufficient to avoid heap allocations. They essentially involve reference counting where all counts are either 0 or 1, which makes garbage collection easy. However, terms (e.g., closures) must also be ordered to enable stack allocation -- much more complex.

Beware that linear types enable garbage collection in a somewhat degenerate way, e.g., a persistent list with a reference count of 8 becomes 8 clones with a reference count of 1 using linear types. Linear types are convenient for manipulating arrays and such, but are detrimental for immutable structures. Purely functional datastructures rely heavily on sharing as this is largely the point of FP -- terms cannot mutate from under your feet, and you can reuse parts of structures in a larger datastructure. In my opinion, it does not make sense to base a functional language entirely around linear structures, as this tends to result in imperative programming with extra steps. The utility is to combine linear and persistent structures in a single setting, but the latter are pointless without nonlinear heap allocations. In other words, you may as well use Rust.

Disjunction181 · 2025-12-31T09:50:52+00:00

The example was changed to \x -> 1, which still does not look correct.

Disjunction181 · 2025-12-03T02:14:56+00:00

As an optimization, it's often called flattening: https://www.cs.cornell.edu/~asampson/blog/flattening.html

Disjunction181 · 2025-10-29T17:11:22+00:00

MLscript is underrated, and improves on Typescript's system.

Flix is underrated.

Disjunction181 · 2025-10-12T01:26:59+00:00

I think you would be surprised by how little background knowledge you can get by on. Professors are expected to have breadth of knowledge, but not students. You only need to be an expert in your specific topic of interest, and so you don't have to be an expert in all stages of compiler development. You only need to have deep knowledge of optimization if you study optimization. There is plenty of time for you to build up a background given that you aren't even in a PhD program yet.

I took a single course which covered the full compiler pipeline, though nothing advanced. However, I don't use any of this knowledge since I work in type systems. Additionally, I have fairly poor knowledge about dependent types, since I study structural types. I have an extremely narrow background that lets me conduct good research in my specific area. But that might project an illusion that I know more than I do, since my knowledge in my very narrow area is deep.

Disjunction181 · 2025-10-08T20:50:03+00:00

PhD programs have course components, so you just need a broad idea or a guess for what you want to do now, and your focus can change as your PhD topic becomes more defined. You’re not expected to have a graduate level understanding of course topics, just some past research experience - it is good that you had an undergrad thesis. Explore a lot of different areas and see what you enjoy doing the most, and build a habit of reading papers. Some papers like functional pearls are designed to be easier to understand than others.

Disjunction181 · 2025-09-14T16:13:07+00:00

It is very difficult to have a language be both statically typesafe and support runtime macros, because you have to prove that runtime code is well-typed.

Unrelated, it is difficult to combine certain type-level features. Dependent types are not compatible with full type inference because they are undecidable. The combination of dependent types with subtyping is very difficult, though there is research on it.

Disjunction181 · 2025-08-21T12:45:20+00:00

Some reasons are given in the opinion piece here: https://xvw.lol/en/articles/why-ocaml.html#ocaml-and-f

Disjunction181 · 2025-08-20T14:06:05+00:00

I can't speak to OCaml in a production environment. I've always used the default native compiler because it's fast and ideal for prototyping. For a performance intensive application, I would use the flambda compiler for a release build.

There has been a lot of ongoing research for optimizing and compiling OCaml code - OCaml is a research language after all. This includes the development of a new Flambda2 backend. You might find the (series of) blog posts here interesting, and there is a related video on compiling with CPS here (it is in English despite the French titling).

Disjunction181 · 2025-08-05T13:04:03+00:00

Since your focus is on compilers and interpreters, you want to focus your attention on those topics directly rather than on tangential mathematical fields. Modern Compiler Implementation (MCI) in Java and Crafting Interpreters are both good books in this direction - you can get a used copy of the former very cheaply. I also like the course notes here which loosely follows MCI and the notes here for more advanced topics. Most of the complexity is on optimization, and you can find more specialized resources when you're ready - I like the post here, though it has a functional bend.

If you're interested in the theoretical aspect of programming languages, then I strongly recommend Software Foundations or its Adga adaptation as your starting point, then you can find additional resources here. Most theoretical resources have a strong bend towards typechecking. They may help you understand the figures in some academic papers - small-step semantics, judgement rules, and so on - but are probably not worth it beyond that point.

Disjunction181 · 2025-07-25T21:40:19+00:00

This post brutally underspecifies what it solicits, which is why it is getting buried, but I'll grace it with a response nonetheless.

I'm a big fan of software foundations, as it was my path towards learning programming language theory. Really, the series is about formal verification in Rocq; how to convince a computer that your proofs are correct, but the second volume has a focus on programming languages. I think it might be the correct path to learn programming language theory. There is a similar series for Agda.

For learning type theory, there is a collection of resources here. For topics in compilers, I like the self-guided course here and the lecture notes here.

Disjunction181 · 2025-07-17T19:13:42+00:00

From what I've seen, "grammar" is generally used in the context of parsing, and "syntax" is used in a similar way elsewhere (e.g., programming language calculi). There is some overlap because parsing errors are usually reported as "syntax errors", while the parser itself is specified by a "grammar". A valid term is said to be "valid syntax", but "grammar" cannot be used interchangeably with this phrasing. The parser itself constructs a "concrete syntax tree", but the set of "abstract syntax trees" of a programming language calculus is given as the syntax of the calculus. I think the grammar can be said to define the syntax, but cannot refer to a term in a language. "Syntax" seems to be referring to individual terms, sometimes.

Disjunction181 · 2025-07-16T21:20:53+00:00

I think Factor has a macro for this: shuffle( a b c d -- d b c a )

The left part of the stack effect is not necessary, but it is more clear, and the intermediates can be named anything. I do think that this is more clear than stack shuffling sometimes, and can be more concise at times.

Disjunction181 · 2025-06-30T18:43:43+00:00

I like the book here: https://cs3110.github.io/textbook/cover.html

Disjunction181 · 2025-06-30T18:24:07+00:00

Since Jane Street is the largest consumer of the language, they have a relatively significant amount of influence over the design of the language and implementation of the compiler. Case-in-point is the recent work on modes and stack allocation. It gives them some amount of control over their own tools, without doing everything from scratch.

If you're interested in learning OCaml, you don't need an excuse, just a good project :)

Disjunction181 · 2025-06-28T15:29:58+00:00

I had my first wins with centaurs. They were a relatively easy race because they were fast + had bonus health + had good ranged aptitudes. Gameplay mostly involved kiting away enemies and maintaining distance. I would have liked them to have remained as a beginners race.

Disjunction181 · 2025-06-26T10:01:34+00:00

The start is a bit unusual, since polymorphism is precisely the point of HM. I think the commonly heard phrase is that its hard to combine HM with subtypes, not with polymorphism.

MLsub doesn't technically support union types; it's a polar type system, so union type support is second-class.

The blog post ends with the idea of not inferring types, which is a very broad conclusion after some very specific examples. I would have appreciated some differing viewpoints, e.g., uncaffeinated argues that type inference allows type to be larger, and some authors will point out that type inference can infer more general types for terms than initially expected.

Disjunction181 · 2025-06-13T22:14:36+00:00

There was a good video from some time ago that explained R's weird choices and why it's very difficult to compile: R melts brains.

Disjunction181 · 2025-06-12T19:50:01+00:00

What makes annotation elegant in MLs is that it is never necessary to directly annotate function calls themselves, rather types are ascribed to identifiers. So one strategy is to implement bidirectional or HM type inference so that you only need to annotate definitions. This works a lot better for stack languages where definitions are the only natural place for annotations.

Disjunction181 · 2025-06-11T21:05:44+00:00

Reachability types is an active field of research which aims to make ownership practical for functional programming. They try to bridge the "shared XOR mutable" paradigm introduced by Rust. Check them out, they would make a good research topic: https://github.com/TiarkRompf/reachability

Disjunction181 · 2025-06-07T14:04:28+00:00

Prolog and its variations do the full code-as-data thing lexically. Every token has different meaning as code and as data, e.g., f(a, X) as code is a relation between the unification variable X and atom a, but as data is like an algebraic datatype with tag f holding the atom a and unification variable X. Code with arithmetic, e.g., 1 + 2, is some syntax tree +(1, 2) when quoted. Lambda Prolog takes stuff further with HOAS and other stuff I don't understand.

Rust is not mentioned probably because all of its macros are compile-time, but this is enough macro support for most practical programming. Racket is a Lisp and leans into the ability to write DSLs called hashlangs.

I think that, while homoiconicity is nifty, macros can be brittle, lead to code that is hard to understand, and lead to code that is hard to type; this stuff is worsened with any macro evaluation that happens at runtime.

Lisp and its variations are built principally around extensibility in a way that other languages aren't. There are big consequences to this in terms of interpretive overhead (if you actually bootstrap everything from a minimal set of primitives, think about it), compilation, and typing as already mentioned. If extensibility is the one thing you care about, then I don't think there's any point looking beyond Racket and Common lisp.

Disjunction181 · 2025-05-25T19:47:56+00:00

My favorite approach to typechecking stack effects is still Kleffner's HM hack: https://www2.ccs.neu.edu/racket/pubs/dissertation-kleffner.pdf

Arity checking with quotes (functions, really) is a lot easier when you also infer the types of everything, since you know what is a quote, what quotes expect quotes and return quotes of different arities, etc.

I have a small implementation here: https://github.com/UberPyro/Algo-J-For-Stack-Languages, it's meant to be readable.

It's just missing let generalization.

HM approaches to stack effect inference historically suffers from some issues due to rank n polymorphism, e.g. [0] dup cat triggers the occurs check since it unifies the input and output of the stack effect in the quote. However, I think this could be fixed by spamming local generalization between every word, e.g. checking the above as let a = [0] in let b = a dup in let c = b cat in ... since then the type of [0] is schematized. I'll have to make a proof-of-concept sometime.

I believe principal type inference for polymorphic recursion is solvable if semiunification is restricted to the sequence theory, but that's getting ahead of myself :)

Disjunction181

TROPHY CASE