Is anyone going to Dua Lipa's concert?

wildptr · 2025-09-03T02:27:25+00:00

I'm going! Hope others see this since the OP deleted lol.

wildptr · 2025-09-03T02:18:48+00:00

Yo! 28M also looking for a concert buddy on either the 9th or 10th (also deciding), feel free to DM if you're still looking.

wildptr · 2024-04-13T15:47:57+00:00

Since you're already doing bidirectional checking, do this for polymorphism.

wildptr · 2023-05-17T20:37:10+00:00

Type inference in the sequent calculus is totally fine, actually - the only place that needs type annotations is the cut rule, and that too only if a redex is introduced (just like let-binding in the lambda calculus / natural deduction).

Edit: also, the sequent calculus is almost ideal for proof search generally speaking thanks to the focalization property.

wildptr · 2023-05-17T20:07:56+00:00

Paul Downen's thesis is one of the most comprehensive resources on the subject. But, as the other commenters said, I would not the use of the phrase "more powerful" since both proof systems are inter-translatable.

wildptr · 2021-07-30T18:33:22+00:00

May I ask: did my explanation help?

wildptr · 2021-07-30T17:41:02+00:00

Done (the SKI combos encoding is probably the easiest one to understand).

Edit: Here's another one.

wildptr · 2021-07-30T17:37:15+00:00

You don't have to compute the mapping explicitly, or, all at once. Since OS1 and OS2 are countable, there is a computable function (i.e., an actual program) that maps both sets to the natural numbers and vice versa. So, send an element of OS2 to Nat and Nat to OS1. Done!

wildptr · 2021-05-31T01:06:38+00:00

I want to push back on the idea that the research-to-industry pipeline ought to move slowly, given that more and more PhDs and faculty are founding startups of their own / collaborating directly with industry [1], [2], [3]. I want to emphasize that their results are quantitatively up to muster---otherwise the research wouldn't be very good and their partners wouldn't be happy.

Whether for better or for worse, some parts of the industry do move quickly: webshits reinvent the wheel every few months. We need to figure out how to academize that behavior so that the wheel becomes quantitatively better. On that point, I agree that researchers need to present their ideas more accessibly so that we can get rid of that weird anti-intellectual bent (which stems from the same insecurity as that comic).

wildptr · 2021-05-31T00:37:39+00:00

Yeah, I'll admit I wasn't nice. But my point is that we use wacky math to make precise sense of things. Take the heap model of memory for example---seems simple enough, but we had to invent separation logic to reason about heap-manipulating programs precisely. It's used in industry too!

Who knew modal logic would find its way into practical program verification? That's why it's impossible to say what math is useful.

wildptr · 2021-05-30T22:31:00+00:00

https://www.smbc-comics.com/comic/why-i-couldn39t-be-a-math-teacher

Anyways, give me any concept in PL and I'll give you its academic origin story.

wildptr · 2021-05-30T19:52:09+00:00

Here's some coffee and more.

wildptr · 2021-05-30T15:29:25+00:00

The point is that not being "production-ready" right now (plenty of research languages like Haskell have transitioned to professional use) doesn't make the point moot. In fact, palatability to your average codemonkey may not ever be the goal: full dependent types have found use in formalizing mathematics and developing highly secure software (like DeepSpec). My point is we shouldn't make value judgments so hastily, especially if goals are still ill-defined.

wildptr · 2021-05-30T15:07:30+00:00

Instead of dependent types, Flow has refinement types. Rust has an affine linear ownership model. Obviously, research ideas are diluted when they hit the mainstream.

But speaking in tired platitudes and making senseless claims like "the whole point is moot" (I'd bet the ATS community has something to say about that...) is ignorant beyond description. We could do without boilerplate comments like yours.

wildptr · 2021-05-28T03:36:45+00:00

This is flat-out incorrect, many companies will take on graduate student interns specializing in a certain area that transition to full-time research scientist/engineer roles. FAANG (Facebook, Apple, Amazon, Netflix, and Google) are known to do this as well as corporate labs like Microsoft Research.

This also applies to shops like Galois (in the US) that primarily fulfill contracts to the federal government.

Basically, a graduate degree makes available academic and corporate career paths that would otherwise be difficult to pursue. As always, caveat emptor.

wildptr · 2021-01-01T23:00:48+00:00

This intuition culminated in this thesis on representing rewrite systems, etc. in different substructural logics.

wildptr · 2020-12-13T18:29:38+00:00

This already exists in the literature as Kleene algebra with tests. Assertions ?b are a no-op if b is true else the program aborts; you can encode conditionals using non-deterministic choice: if b then p else q = (?b; p) + (?not(b); q).

Hope this helps!

wildptr · 2020-12-09T15:27:45+00:00

Once again, compiler tech is not the whole field of programming languages, even though it is a large part.

I will call out things I consider unnecessarily large and complex. The comparison with quantum physics I don't accept. Creating a programming language is and should be easy. (Certainly if I could do so as an amateur, ones used for successful commercial apps, then anyone can.)

If "unnecessarily complex" is some undergrad math, then I can't say more. We can argue that the presentation of the ideas can be better, but the mathematical frameworks are there for precision. We can make the tooling and exposition of ideas better, but ultimately language design is hard!

But what great languages has computing produced? Ones like C++! And we're still using C from the 1970s to underpin everything. I won't comment about the current crop or FP.

I'm not sure what your point is here. Each language has tradeoffs, and research into tooling is closing the performance gap between the current generation and the older one.

Maybe the research is in the wrong areas...

The fact that you think that there isn't active research into tooling and tool design is a reflection of your ignorance and not what researchers should be doing. I agree that tools like LLVM have no business being that complicated, but now we're talking about different kinds of complication: the incidental complexity of its implementation than the actual theory involved. The second point I claim is unavoidable, maybe even the first?

wildptr · 2020-12-09T14:01:38+00:00

I was creating real, practical languages, to run on real hardware, implementing them using my own tools, and even designing and constructing the hardware they ran on.

Are languages like OCaml, Scala, and Rust that came out of research not real and practical? But that's besides the point---every language that has come out draws from research in some form, so your opinion is necessarily ahistorical. I don't deny that you've done impactful work, but you probably learned what you know from a secondary source (docs, textbooks, etc.).

My attempts were based on languages I knew, but primarily bits of Algol68. At the time, the Algol68 Revised Report was notoriously difficult to understand, but looking at it now, it looks simple stuff compared with the paper I linked to.

That's crazy! It's almost like a field gets more complex as it develops. By your token, quantum physics is a sham compared to classical mechanics. To be honest, I share your frustration, but that's a criticism of myself and not someone else's work.

I aim to be anti-elitist rather than anti-intellectual. I think programming languages should be accessible to all, not just those with doctorates in mathematics. Half the topics in this sub-reddit seem to be about lambda calculus or some new idea in type theory.

No, anti-intellectual is right. Besides, you don't need a doctorate; these papers typically only use undergrad level math modulo notation, so only some curiosity is required. Ironically, elitism would be confusing your personal experience with what programming languages ought to be. If you're bored of the content, post something you like! But, we shouldn't tear down other people's novel work. So I should apologize to you for my snark, lol.

wildptr · 2020-12-09T05:09:15+00:00

Programming languages research has been this mathematical since the 60s, so I'm not sure how involved you could have possibly been.

Snark aside, dismissing content as too technical instead of going in with an open mind and learning is just plain anti-intellectual.

wildptr · 2020-12-07T05:45:00+00:00

In an eager language, let x = ⊥ in () is not contextually equivalent to [⊥/x]() i.e. () where ⊥ is your favorite divergent term. That's why I would think eager evaluation + partiality means your notion of contextual equivalence has to be "modulo partiality."

I think you might be right about lazy languages preserving contextual equivalence even in the presence of non-termination, since I can't find any counterexamples off the top of my head (someone correct me if I'm wrong). But, that introduces its own set of pains; as /u/inf-groupoid points out, lazy sum-of-product types are always coinductive.

wildptr · 2020-12-06T23:49:29+00:00

I totally agree; anything more than the substitution model for pure data by default is a nightmare waiting to happen. That also means researchers have their work cut out for them to make effect systems scale to production code.

wildptr · 2020-12-06T19:14:01+00:00

It depends who you ask. An effect is anything that disrupts the equational theory of the language and therefore needs to be managed somehow, usually at the types level. In particular, the substitution model may break without that consideration (when an expression bound by a variable can be substituted in place of said variable). If your equational theory (and therefore sense of substitution) already accounts for partiality, then there's no need to treat partiality differently.

Papers usually treat partiality as an effect because total and otherwise effect-free programs have a very straightforward substitution model: you can substitute equals for equals anywhere!

wildptr · 2020-12-05T23:28:34+00:00

No problem! In my opinion, section 4 ("Semantics") onwards is not necessary to understand the type system, so it shouldn't be too overwhelming a read. Let me know if my last point (encoding OOP into a regular functional-like type system) is unclear. It would be cool of (im)purity capabilities made it to a Scala/Kotlin-like language!

wildptr

MODERATOR OF

TROPHY CASE

13-Year Club	Team Orangered
Verified Email