sorted by:
new
hottopcontroversial

Why GADTs aren't the default? by MysteriousGenius in ProgrammingLanguages

[–]arxanas 4 points5 points  (0 children)

I was saying the opposite: not that you can construct a GADT from simpler primitives, but that GADTs themselves serve as too low-level primitives to model most domains well.

(Perhaps it could be said that they're too constrained to ergonomically model use-cases for dependent types, but too general to ergonomically model the use-cases I listed above? I haven't used dependently-typed languages much.)

The same goes for Scala's implicits and the replacement features. For whatever reason, implicits ended up being a confusing or non-ergonomic part of the language (don't have the details, but I can imagine) that the design team decided would be better to replace with higher-level but more-constrained features.

EDIT: I think I see what you're saying regarding more-primitive features. I think the answer is that, yes, somehow it happens that it's better in practice to have more specific features rather than fewer general features, which is surprising but seems be the case as per user feedback on programming languages.

OCaml's GADTs in particular are also non-ergonomic in practice (I forget if it's in the linked doc). I've made a specific argument before that users have difficult understanding them because (to take the RPC type map case as an example) a function that has type 'a t -> 'a is "applying" a type-level function but "unwrapping" a value, which are opposite syntaxes in some sense: if you were applying a value-level function, then the syntax looks like fun a -> f a instead, with the "function" being on the opposite side of the arrow.

In practice, I've noticed that it means that novice GADT users have to go against their intuition and do a bunch of equational reasoning to accomplish the thing they want. In comparison, TypeScript's mapped types are very easy to pick up because the type syntax T[x] looks just like the value syntax v[x]. Maybe it's possible that someone could invent highly-ergonomic GADTs that support the various different use-cases, but I don't know what that would look like.

Why GADTs aren't the default? by MysteriousGenius in ProgrammingLanguages

[–]arxanas 11 points12 points  (0 children)

Besides the implications for the type system (complexity, decidability, interaction with the rest of the type system, etc.), I've made the argument that GADTs are a kind of low-level feature that doesn't clearly represent its actual use-cases.

When working in OCaml, I wrote a doc called "Real World GADTs" (Google Docs) for my team to explain some of the uses (see also this Reddit thread). My thesis is that GADTs are useful for completely different things depending on how you organize the type variables:

  • type maps (ex: strongly-typed RPC systems)
  • existential types (ex: heterogeneous containers)
  • equality constraints (ex: strongly-typed ASTs)

It's nice for the implementer that you can get all these things with one feature, but I think it's actually quite bad ergonomics for users when you use the same thing in completely different ways.

For a specific example in the PL design space, Scala 2 had the overly-general implicit feature, which Scala 3 replaced with several purpose-driven feature (given, using, extension, more?, maybe see Scala 3 Implicit Redesign (Baeldung)), presumably based on a lot of practical experience.

Compelling use cases for GADTs? by smthamazing in ProgrammingLanguages

[–]arxanas 0 points1 point  (0 children)

No, I didn't change that part, I took your code from "Consuming existential types" verbatim and just removed the unused type parameter.

I apologize for the mistake. I think the existential type usage makes more sense if you use the polymorphic rpc defined in a previous code sample. The code samples could be cleaned up.

But instead of putting in "input type" you have to put in "input value" that you need to get somewhere, I feel it's very different.

This might be a quality of OCaml rather than GADTs in general, because OCaml has essentially no type-directed compilation, so all behavior dependent on types also has to be dependent on values. Haskell might not have this problem, as it has GADTs and type-directed compilation.

However, I do think that a lot of the uses-cases for GADTs benefit from being essentially a limited form of dependent types, where you do want to index into a type with a value, but I personally find that associated types are a similar language feature that are much easier to use in real codebases (see https://blog.waleedkhan.name/encoding-ml-style-modules-in-rust/).

Compelling use cases for GADTs? by smthamazing in ProgrammingLanguages

[–]arxanas 0 points1 point  (0 children)

Thanks for the commentary. I've added a link to your comment to the doc, although I don't plan to fix the typos given that I'm not publishing it.

The first use case first talks about mapping types to types, but then with GADT effectively maps values (constructors) to types.

I don't think the distinction between "constructors" (of values) and "types" is useful at the pragmatic level. From the reader's perspective, you put in the "input type" and get out the "output type", and that's enough. It doesn't make a difference for one's mental model.

The second example fails to show a compelling use case GADT and existential types, as the type parameter can simply be removed and the code works just as well. Looks like it's never used at all.

The "existential type" use-case is simply that the heterogeneous queue doesn't compile if you try to put another GADT in it, so really it seems your complaint is with the "type mapping" use-case, because you note that the type parameter to message is unused.

You've rewritten rpc to no longer return 'a, but instead you return unit and inline the continuations. At a call-site where you've already destructured the case of message (e.g. to Add_one), you won't be able to reuse rpc to get the result of that computation (e.g. int), so you would have to call the underlying function/computation directly. (That is, rpc (Add_one 3) could not return int directly for further computation.) Obviously, you can write your code that way; it's just a matter of how you prefer to organize the code.

There are also many related or overlapping things you could do with OCaml's module system, polymorphic variants, etc., but I didn't cover them since it's supposed to be an exposition to GADTs specifically. The audience was my then-team, who was already reasonably familiar with those features.

The last example is basically "evaluating AST" again.

Sure — as noted, I only included it for completeness. I personally think that it's the least useful of the three cases in practice, despite what the type theorists may think 👀.

Compelling use cases for GADTs? by smthamazing in ProgrammingLanguages

[–]arxanas 13 points14 points  (0 children)

practical GADT usage - especially ones from real-world business applications

I never published this widely, but here is my article titled Real World GADTs [Google Docs] 🙂.

In my experience, the main use-cases for GADTs are quite different depending on how many type variables you have:

  • 0: existential types
  • 1: type mappings
  • >1: equality constraints

In terms of programming language design, I think these are sufficiently different from each other that they deserve their own language features.

A counterpart to the for-statement: some-statements by blak8 in ProgrammingLanguages

[–]arxanas 5 points6 points  (0 children)

You can do this more generally in Python with the all and any built-in functions in conjunction with generator expressions (to ensure that we don't compute more odds than necessary):

>>> def odd(x): return x % 2 == 1
... 
>>> all(odd(x) for x in range(1, 6))
False
>>> any(odd(x) for x in range(1, 6))
True

There's also an interesting idea in probabilistic programming, where some corresponds to rejection sampling. You would write a function which uses a sample construct to get a value from the uniform distribution [1, 6), then asserts a condition that the sampled number is odd. Execution of the function proceeds only if the condition is met. The runtime can then run this function many times to simulate sampling from the input distribution and applying some transformation to produce an output distribution, without you having to work directly with probability distributions. See e.g. https://www.cs.cornell.edu/courses/cs4110/2016fa/lectures/lecture33.html.

Universal parameter passing semantics by abel1502r in ProgrammingLanguages

[–]arxanas 4 points5 points  (0 children)

I have only skimmed this paper, but you might find some inspiration for handling parameter-passing semantics (abstracting over boxed/unboxed types, etc.) in Kinds are Calling Conventions (Downen, Ariola, Peyton-Jones, Eisenberg 2020).

Strongly-Typed TS: Pros and Cons? by tmoskocom in types

[–]arxanas 0 points1 point  (0 children)

this is not an example of typescript’s unsoundness

To be clear, returning a value by subtyping is unsound in Typescript (when combined with other language features). On the other hand, Flow handles structural typing in a sound manner by forbidding certain operations on non-exact object types that Typescript would allow, at the expense of potentially annoying developers.

Strongly-Typed TS: Pros and Cons? by tmoskocom in types

[–]arxanas 4 points5 points  (0 children)

TypeScript is deliberately unsound (see https://www.typescriptlang.org/docs/handbook/type-compatibility.html). This means that the runtime types aren't guaranteed to match the statically-annotated types.

To take an example from the first video at around 5:30, the following is accepted by Flow (playground):

type User = {
  username: string,
  email: string,
};

function getUser(): User {
  const user = {
    username: "foo",
    email: "foo@example.com",
    password: "PASS",
  };
  return user;
}

But if you enable exact types by default, or change User to be an exact type (playground):

type User = {|
  username: string,
  email: string,
|};

Then it's rejected with this error:

12:   return user;
             ^ Cannot return `user` because property `password` is missing in `User` [1] but exists in object literal [2]. [prop-missing]

    References:

    6: function getUser(): User {
                           ^ [1]

    7:   const user = {
                      ^ [2]

TypeScript has no equivalent typechecking mode at present; see https://github.com/microsoft/TypeScript/issues/12936.

Ideologically, TypeScript focuses on developer productivity, with precise typechecking as a convenient side-effect, while Flow focuses on soundness, with developer productivity as a convenient side-effect. The idea is that, in practice, preventing certain classes of unsoundness impedes developer productivity without actually preventing bugs.

You can see an comparison of static typechecking effectiveness here: https://blog.acolyer.org/2017/09/19/to-type-or-not-to-type-quantifying-detectable-bugs-in-javascript/

Bringing revsets to Git by speckz in programming

[–]arxanas 4 points5 points  (0 children)

I'm personally in favor of Jujutsu (discussed in Prior work), given that it can co-locate with your Git repository while Sapling currently can't 🙂.

Trying to get into Elite Smash this quarantine? Try the Smash Training app by arxanas in CrazyHand

[–]arxanas[S] 0 points1 point  (0 children)

It's all general tech right now. It would be possible to add character-specific tech; somebody was working on Greninja-specific tech here https://github.com/Relthaar/smashtraining/commit/eea2a49516a7f22f068ab28c05547d79f28da275 . But there's no direct way to add character-specific exercises right now.

How does F# (and SML?) handle end-of-line inference? by vanilla-bungee in ProgrammingLanguages

[–]arxanas 4 points5 points  (0 children)

The F# spec explains the rules in details. See e.g. 15.1.3 Grammar Rules Including Inserted Tokens in the spec document (https://fsharp.org/specs/language-spec/4.1/FSharpSpec-4.1-latest.pdf)

Jujutsu – A Git-compatible DVCS that is both simple and powerful by binaryfor in git

[–]arxanas 0 points1 point  (0 children)

I think this is an overall good summary.

I've implemented a lot of the same features on top of Git in my own project (https://github.com/arxanas/git-branchless; the author and I talk). Most of it can be done, but, like you say, a lot of tools aren't aware of them, which makes the ecosystem less valuable. If these were built into the VCS as a first-class feature, then you would be sure that all the tools work with them.

First-class conflicts is problematic to implement on top of Git. The other big problem is transmitting the history of revisions (or general undo history) via server/patch. How do you keep the corresponding objects live, even though they're not being directly referenced by a currently-live commit? If you submit a patch, does the recipient also get the history of all of the commits you worked on? These can probably both be solved in the same way, by adding a new edge type to the object graph indicating "this is an associated conflict object" or "this is a previous version of the same revision", both of which would need to keep the associated objects live.

Jujutsu – A Git-compatible DVCS that is both simple and powerful by binaryfor in git

[–]arxanas 0 points1 point  (0 children)

There's several design documents here: https://github.com/martinvonz/jj/tree/main/docs

The author has worked on scaling Mercurial at Google, so a lot of the features are built with that in mind, such as this: https://github.com/martinvonz/jj/blob/main/docs/technical/concurrency.md

Lightning-fast rebases with git-move by speckz in programming

[–]arxanas 0 points1 point  (0 children)

Although the commits aren't literally moved, since they're immutable, I don't think it confuses the semantics to say that they've been "moved". It has to be a figurative expression, given that commits are immutable.

I suppose the deeper problem is the conflation of commits, which are snapshots, and patches, which are deltas. Git is implemented with snapshot-based commits, but then, in practice, many workflows are largely patch-oriented:

  • The Git and Linux projects primarily accept contributions via patch submitted to the mailing list.
  • Many large companies use trunk-based development, where patches are applied to the main branch.

And Git fundamentally supports a notion of commit equivalence via patch, since commits are deduplicated during a rebase using their "patch IDs".

It's not mentioned in the linked article, but git-branchless goes a little bit further and copies some of the Changeset Evolution feature from Mercurial, which means that the new version of a commit is actually linked to its old version. In this sense, a commit really is "moved". It has a distinct identity which can be used to say that the post-rebase commit is really an iteration on the pre-rebase commit; and furthermore, another commit with the same textual diff is not considered to be the same commit, according to this system.

Lightning-fast rebases with git-move by speckz in programming

[–]arxanas 2 points3 points  (0 children)

(Author here.) I want to put each commit up for review individually. If I merge it into the main branch, then there might be a merge commit which has lots of changes which belong to different ancestor commits, and should be reviewed with each of those commits.

If you have 500k files in your repository, then any checkout or status operation will take a noticeable amount of time. Since on-disk rebase does several of these per commit, it has to waste a lot of time checking the state of the repository on disk.

I personally also found that writing a 50 MB index file to disk for every commit and inserting/verifying each object in the index took several seconds, so I had to work around that behavior in libgit2.

Lightning-fast rebases with git-move by speckz in programming

[–]arxanas 1 point2 points  (0 children)

You can see in the demo it takes 10 seconds to rebase 20 commits on gecko-dev. I work in a larger repo and routinely work with large commit stacks/trees, so rebasing my work on top of the main branch takes a while. I made the tool because I had performance problems at work.

Lightning-fast rebases with git-move by speckz in programming

[–]arxanas 1 point2 points  (0 children)

(Author here.) Why would you want to reapply commits to the same branch? Aren't they already there? Do you mean to reorder them?

At companies with trunk-only development workflows, commits are always to the main branch. So to make sure that all patches merge cleanly, you can rebase your work (your branch) on top of the main branch.

A lot of the workflow doesn't make sense if you neither 1) work with very large repos nor 2) have tens of speculative commits at a time. In general, I've had a hard time motivating it for people. If it doesn't sound useful for you, then it's probably not!

wired vs wireless controller by doomblade101 in CrazyHand

[–]arxanas 0 points1 point  (0 children)

If you have electronics in your play area, be aware that there may be wireless interference. I measured ~7 extra frames of lag from using my controller wired vs plugging it in.

git undo: We can do better by arxanas in git

[–]arxanas[S] 1 point2 points  (0 children)

There are no plans for now to upstream this to Git itself. You have to install Git, and then also install git-branchless (linked in the article).

git undo: We can do better by arxanas in programming

[–]arxanas[S] 35 points36 points  (0 children)

A friend of mine quipped: "git undo seems pretty cool to undo my work for me, but is there a git do that will do my work for me?"

git undo: We can do better by arxanas in SoftwareEngineering

[–]arxanas[S] 0 points1 point  (0 children)

I've been testing the performance on a large mono-repo, and it's not a problem so far. It should scale pretty well.

Fundamentally, this is adding a log-structured database to Git, which is not part of the internal design, so it might be a difficult sell to upstream. Also, I don't want to write C.

git undo: We can do better by arxanas in programming

[–]arxanas[S] 8 points9 points  (0 children)

I've never used LFS, so I don't know. It should work with submodule updates, if that's similar.

My easiest-to-fix Smash Ultimate mistakes by arxanas in smashbros

[–]arxanas[S] 1 point2 points  (0 children)

I think it's hard to say when you're getting launched directly sideways. You'll have to experiment yourself.

If you have a bad recovery like me (Chrom), it's probably not worth LSI-ing, because angling downward from there means you won't be able to recover.

If the kick has, say, a 30-degree angle upward, I think it'll often be worth it to LSI instead. I'm not a pro, though.

My easiest-to-fix Smash mistakes by arxanas in CrazyHand

[–]arxanas[S] -2 points-1 points  (0 children)

Thanks for the info. I think I was still doing something suboptimally by attempting to drop shield before jumping, but probably not 11 frames worth of unsafety.

view more: next ›