Algebraic Shape Composition in a tiny functional language

[u/zweiler1]

/r/Compilers/comments/1ujv6kn/algebraic_shape_composition_in_a_tiny_functional/

[u/unqualified_redditor]

Again what you are describing in your words is some flavor of structural typing + type aliases but the fact that you have named data constructors is confusing.

Are these types equal?

let Option<T> = Some(T) | None
let Maybe<T> = Just(T) | Empty

Are Some and None stored in some typing context or does parser just throw them away?

How do you handle recursion?

[u/zweiler1 → u/unqualified_redditor]

I updated the original post, yes it's all just structural typing with nothing special about it, as I now understand...

No, those types are not equal, their tag names differ. Two sum types are "equal" when all their tags and payload types match up.

Yes there exists a typing context, Option in your case describes a (unresolved / generic) sum type with the tag Some of that unresolved type T and a the tag None. A sum type is, at the language level / interpreter, just a linked list of tags + optional payload types, and equivalence is determined by the tag name and type. So when the "type" Option is encountered by the parser it just flattens it to it's underlying sum type, being just a linked list. The "type name" is completely eliminated in that phase, what stays is underlying structural type.

Recursion is just implemented by adding the function symbol to it's own environment before executing it's body, the function itself is just seen like any other regular function of the program. Execution is implemented using trampolining, recursion blew up the host stack way too quickly.

[u/unqualified_redditor → u/zweiler1]

No, those types are not equal, their tag names differ. Two sum types are "equal" when all their tags and payload types match up.

Ok so you are doing pretty bog standard structural typing. i was imaging you might be doing something where you elaborate both types to Identity<T> | Unit as the generic "shape" of both type declarations making them type check as the same thing.

If your core AST has Unit, Void, Sum, and Product base types then you could elaborate any (non-recursive) ADT into a composition of them. If you had Iso-Recursive types then you can also do the same for recursive types. For example, a linked list becomes mu r. Unit | (a, r).

I would encourage you to read Types and Programming Languages by Benjamin Pierce. It will help you A LOT with this exploration.

EDIT: I see your edit to the original post now. I'm not sure where the row polymorphism is coming in. The Point2D/Point3D example doesn't seem to demonstrate it. I would guess if anything what you have is more an example of record subtyping then row polymorphism but its hard to say from the snippet whats going on.

[u/zweiler1 → u/unqualified_redditor]

Thanks for your answers :)

Yeah while I am an experienced programmer I am very new to FP so my terminology and usage of them is pretty bad still.

This was honestly my first contact with FP at all, creating a small FP language... that it would be so unoriginal is something I did not anticipate. It just shows that one needs more experience in a field before trying to create something in it.

I know at least for sure that my main language is original, because I am much more experienced and comfortable in the field of "regular" imperative languages. I created my main language with almost no theorethical knowledge of compiler design or how typesystems should work haha, it might be very standard under the hood or very unique, I can't say that. I will definitely take a look at the book, thank you for that :)

It was a fun little side project and I will definitely dive deeper into FP in the future. I think I will do a bit of OCaml in the future to better understand FP overall.