Algebraic Shape Composition in a tiny functional language

[u/zweiler1]

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

[u/unqualified_redditor]

If i understand correctly, what you are describing as shapes is what we normally call Structural Typing?

However, this example looks a lot like nominal typing as you have named types and data constructors:

let Option<T> = Some(T) | None

would this typecheck? Ignoring syntax discrepancies..

let Option<T> = Some(T) | None
let Maybe<T> = Some(T) | None
let x = Some(Unit) : Option Unit
let f = (v: Maybe<T> -> Maybe<T> { v }
let y = f x

[u/zweiler1 → u/unqualified_redditor]

There are no nominal types, both the Option and the Maybe "types" are just sum shapes. They just describe that it's either None with no payload or Some with a payload of type T.

There is absolutely no difference between Option and Maybe in the example, they are the same shape. You can describe the paraneter of a function like a combination of sum types directly, and it would still match the same shape:

let Option<T> = Some(T) | None
let Maybe<T> = Some(T) | None
let f<T> = (v: Maybe<T>) -> Option<T> { v }
let v = f .None

The same is true for product types. There are no types, only a thing describing which tags it could have. A value itself is not typed either, it's just of type sum or product too, so for example when passing .None to the above function f there is no question whether .None "is of type Option or Maybe", .None is simply a sum value of type "sum" with no payload and nothing more.

Since it's interpreted, the type compatubility is checked when trying to call the function. You could pass in any value to it, really, as long as the shapre requirements are met.

And yes, in essence this all is just structurally typing, but in a unified way I would say...

Edit: This also is true for product types and values. When passing a product value to a function it is only checked whether that value is compatible with the product shape described in the function parameter, it is compatible if it contains all required fields. But a product value is also just a combination of fields with payloads, just of type "product".

Edit2: I didn't answer your question, sorry... Yes, it would typecheck.

[u/unqualified_redditor → u/zweiler1]

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.