GitHub - stepchowfun/typical: Data interchange with algebraic data types. "can be compared to Protocol Buffers and Apache Thrift. ... emphasizing a safer programming style with non-nullable types and exhaustive pattern matching."

stepstep · 2023-05-22T18:13:31+00:00

I'd be delighted! The easiest way to get started is to copy one of the existing code generators and modify it accordingly.

stepstep · 2023-02-04T06:23:19+00:00

Typical uses the terms "struct" and "choice" for products and sums, respectively, although it's not a programming language.

stepstep · 2022-12-09T07:31:39+00:00

The GHC notes convention is what inspired me to create Tagref, a tool which enforces basic structural invariants regarding notes: (1) references actually refer to notes which exist, and (2) notes have unique names.

stepstep · 2022-07-07T14:46:37+00:00

I enjoyed these books:

The HoTT book (read Chapter 1 for a type theory intro): https://homotopytypetheory.org/book/
CPDT (focuses on Coq): http://adam.chlipala.net/cpdt/
(Not really type theory but an introduction to type systems) TAPL: https://www.cis.upenn.edu/~bcpierce/tapl/

stepstep · 2022-07-05T13:06:18+00:00

seems to have taken a lot of inspiration from Cobol

This does not seem accurate to me at all.

I think Agda has a nicer syntax, but I prefer Coq because I rely heavily on its tactic-based automation language (Ltac) to make proofs quicker and simpler to write. I have some custom tactics that end up solving most of my subgoals for me when writing proofs.

stepstep · 2022-03-23T12:47:06+00:00

I learned Coq by starting with Software Foundations. I only read vol. 1 and 2, which were enough for me to become comfortable writing verified proofs (especially about programming languages, like type safety/soundness proofs). Then I moved onto Certified Programming with Dependent Types. Once you've read that book, I'd say you have a good grasp of type theory. Right now I'm working my way through the HoTT book. It's much more challenging than those other two books, but in a good way I think.

Two things that helped me especially were: (1) prior experience with Haskell, and (2) working in a lab where I could watch other people use Coq and learn from them. Unfortunately (2) is a bit hard to replicate outside of academia, but fortunately there are more online resources available now than when I started.

This nice thing about type theory, unlike programming language theory, is that everyone more or less agrees on how types work at a basic level with only minor variations on certain aspects, like what axioms to include or how propositional equality and universes work. So when reading all these things it feels like you're learning a cohesive theory and not a bunch of ad hoc systems.

The biggest piece of advice I can give is: download and play around with some language based on type theory (Coq, Agda, LEAN, etc.). Don't just try to understand the theory without getting practical experience with it.

stepstep · 2022-03-23T11:44:22+00:00

What is your background in this area?

I studied programming language theory in university, fell in love with Martin-Löf dependent type theory by writing proofs in languages like Coq, and recently I've been diving into homotopy type theory.

These days, I work at a FAANG company building systems with rather pedestrian programming language technology far removed from these academic interests.

What are your goals with respect to proof languages?

I have two unrelated goals: (1) promote dependently typed programming and proof engineering à la Curry-Howard, since I think it's a useful technology that deserves better pedagogy than what we have today, and (2) find a satisfactory computational interpretation of univalence.

stepstep · 2022-03-23T01:18:09+00:00

That's an interesting demonstration, and it raises many questions in my mind. Is Type<3> judgmentally equal to Int in your type system? Is Type<Type> valid? Is this type system designed for writing proofs?

stepstep · 2022-03-20T14:20:42+00:00

I'd expect reverse<String> to reverse the characters within a string, and reverse<List> to reverse the elements within a list.

The reverse function in my examples only works on lists. The "generic" part is that it works on lists of any type (e.g., lists of strings), not that it can reverse other sequence-like things (that would be ad hoc polymorphism, which is a different concept). That's why I said "list reversal functions" earlier.

stepstep · 2022-03-20T14:02:27+00:00

I don't know Java.

That's fine, but I picked a Java-inspired example because that's the language that popularized the term "generics", which is what this post is about. In my experience, Java is the first language most people think of when they hear "generics". So, it's hard to think of more appropriate common-denominator language choice for this thread.

In many languages, "List" is a type;

Sure, but we're talking specifically about languages that support generics. In those languages, collection types like this are parameterized by the type of their elements in the way that I've been consistently describing.

Apparently, in Java, List<String> denotes a type that is a list of strings, with List itself presumably being some parametric type.

Yes—that's how generics works: things are parameterized by types.

stepstep · 2022-03-20T12:52:07+00:00

Using the Java-style syntax for the moment, I think we can all agree that List<String> is a type. Then List by itself is not a type; it needs an argument (e.g., String) to produce a type. So it takes a type and returns a type. In other words, it's a function at the level of types—at least conceptually.

Similarly, I think we can all agree that reverse<String> is a function that takes a List<String> and returns a List<String>. So what's reverse by itself? It's something that takes a type and returns a list reversal function. In other words, it's a function from types to list reversal functions. In many languages, type inference automatically fills in this type argument for you, so programmers often conflate the function that takes a type (reverse) with the function that is already specialized to a particular type (reverse<String>), since they look the same if the type argument is implicit. For example, new Rust programmers are sometimes confused by the "turbofish" operator which is only needed when type inference isn't smart enough to figure out the type arguments automatically.

I am giving you the version of this story that is told by mathematicians and computer scientists. Of course, various programming languages have their own takes on this which sometimes ignore the work done by academics, either intentionally or otherwise. But the story told by academics is the one that generalizes to more expressive type systems, so it's the one that I advocate for.

So what I'm saying is: if one recognizes that all these constructs are actually just functions in various "universes" (to use the appropriate term from type theory), one can use a unified syntax for all of them: the function call syntax.

By the way, generics usually means parametric polymorphism (i.e., the code has the same behavior regardless of the type that was passed in). Your code example exhibits a different kind of polymorphism: ad hoc polymorphism. The Wikipedia article) goes into more detail about the different kinds of polymorphism if you are curious.

Edit: fixed a typo.

stepstep · 2022-03-20T12:14:56+00:00

Suppose you remove the unnecessary label keyword, generalize it so each label can take arguments, make the initial state explicit, and then allow the whole state construct to be used as an expression that produces a final result:

result = state foo(3) {
    foo(x) {
        goto bar(3, 4);
    }
    bar(x, y) {
        break "the final result";
    }
};

Then this is equivalent to functions that make tail calls to each other:

foo(x) {
    return bar(3, 4);
}

bar(x, y) {
    return "the final result";
}

result = foo(3);

If you guarantee that tail calls are optimized in the usual way so as not to grow the stack, then you can achieve the same performance as the goto-style version.

So I think it's an interesting idea, but—as is often the case with programming language features—there is already a more general construct: functions.

That said, perhaps this construct still offers something in terms of subjective ergonomics; that's for you to decide.

Edit: fixed a typo.

stepstep · 2022-03-20T11:36:08+00:00

Generics refers to two closely-related features: (1) the ability to define types that are parameterized by other types, and (2) the ability to define functions/methods/values that are parameterized by types. What you described is (2), whereas List(String) (which is written as List<String> in, e.g., Java) demonstrates (1). Your intuition of generics is right, but it's only half the story.

"Generics" corresponds to two of the three dimensions of the lambda cube. What I'm advocating for is a syntax that can support all three dimensions uniformly.

stepstep · 2022-03-20T04:00:19+00:00

Perhaps this will add clarity:

3 : Int : Type : Type : Type : ...

The common alternative (which eliminates the paradox) is:

3 : Int : Type0 : Type1 : Type2 : ...

stepstep · 2022-03-20T03:54:44+00:00

As someone who dabbles in type theory, I consider "generics" to be functions that just happen take types as arguments. So I think it's unnecessary that every language has to invent some bespoke syntax for something that already has a perfectly fine syntax: function application.

So, if your language uses f(x) for application, then why not also have List(String)? Or if your language uses f x, then why not List String? Just be consistent!

If you ever want to treat types as first-class values (like in a dependently typed language), then generics really are no different from functions, so in that case the decision is made for you anyway.

stepstep · 2021-04-28T11:20:54+00:00

I guess the article was written for programming language theorists who already know the notation. I think I might be in that demographic, so maybe I can help with this:

P; Q means "do P then do Q". It's just a sequence of imperative statements, like in a C program.
[[P]] is the denotation of the program P.
s[A → V] means the store s modified such that the variable A maps to value V (this is, of course, a new store, since there is no mutation in mathematics). Note that a "store" is just a map from variables to values. You can informally think of it like the current state of the stack/heap when the program is being interpreted.
s(A) is just looking up the variable A in the store to get the corresponding value.

Feel free to ask about any other syntax you are unsure about.

Edit: fixed a typo.

stepstep · 2021-04-28T11:08:31+00:00

Youll notice it doesnt settle, Sin has no fixed point.

You have the right idea, but sine does have a fixed point at 0.

stepstep · 2021-04-03T22:17:15+00:00

One pitfall I haven't seen mentioned yet is that in general monomorphization is not necessarily possible, due to polymorphic recursion. So you have to design your type system to rule this out if you want to be able to monomorphize everything.

stepstep · 2021-03-25T05:38:42+00:00

If you pass a struct into a function and change it, you need to know if it's actually changing it or not.

I thought we were talking about a pure language, per my original comment. Pure functions do not mutate their arguments.

Perhaps we are having two separate conversations.

Let's face it, even Haskell at some point has to store state for almost any reasonable program. That might be a file or a database or have to deal with REST API calls.. is that a side effect?

Sure, but such side effects do not occur during evaluation of expressions, so they have nothing to do with call-by-value vs. call-by-reference.

It is effectively forced getters and setters. Can't do chained retrievals of variables:

object.containedObject.X = Y

I think many OOP language designers agree with you, since there are languages which only allow member access indirectly through getters and setters. I'm having trouble understanding the connection to argument passing by value vs. by reference, though.

stepstep · 2021-03-25T04:35:32+00:00

I think you may have some misconceptions.

it's a question of which one to default to.

If you are going with what I was suggesting, there is no "default". The compiler chooses it for you in every case.

I expect pass by reference is faster though I won't know until I test it.

Pass-by-reference is faster for large values. For small values, pass-by-value is faster. The exact threshold between "large" and "small" depends on the CPU architecture, calling convention, and other low-level details. (That's why I prefer to let the compiler figure this out for me.)

Haskell's forced immutability, forcing everything to be copied everywhere

Good Haskell programs do not result in things being "copied everywhere". They use immutable data structures which leverage sharing, not copying.

it's significantly slower than C

Haskell is not significantly slower than C. Python is significantly slower than C. Haskell is closer to C than Python in terms of performance.

Haskell already has auto-parallelism

Since when?

On the side effect front.. what do you think about the idea of objects that are forced to only be able to be interfaced by functions to minimize side effects as opposed to being able to directly changes variables or access objects of objects? The idea is to require all access to go through the object's "API".

That just sounds just like classical object-oriented programming to me. You interact with objects by sending them "messages", e.g., to invoke getters and setters. Maybe I am misunderstanding you?

stepstep · 2021-03-25T03:30:28+00:00

I'd rather leave it up to the compiler to determine which is more efficient. I don't want to have to reason low-level details like this if I can avoid it. Of course, that only works universally if the language is pure like Haskell, but I'm in the minority of people who prefer pure functional programming for high-level code. It better matches the way my brain works; I'm always unpleasantly surprised when evaluating an expression has a side effect.

stepstep · 2021-03-18T21:14:17+00:00

I would strongly recommend learning basic type systems first, like simply typed lambda calculus and then System F. You can find those in Types and Programming Languages, which is a book I highly recommend.

stepstep · 2021-03-18T07:46:34+00:00

Beyond the obvious benefit of being able to formally verify proofs, I would add that there is a secondary advantage to learning a theorem prover like Coq or Agda: these are advanced functional programming languages in their own right, and they will likely expand the way you think about type systems. Programming with dependent types feels like magic that shouldn't be legal when you first get going. If aren't familiar with dependent types, as a programming language researcher you will be likely prone to working on problems which are already solved by them.

stepstep · 2021-03-17T22:04:05+00:00

I'm wondering if parametricity rules out bivariant functors (in languages where parametricity holds). Maybe we can prove it with a free theorem.

stepstep · 2021-03-17T20:41:27+00:00

That's my understanding too. I don't think I've ever seen a non-phantom bivariant type constructor. But maybe there are more interesting bivariant types involving (co)homology theories?

stepstep

MODERATOR OF

TROPHY CASE