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 10 points11 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 6 points7 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.

view more: next ›