search

johnynek / bosatsu

A python-ish pure and total functional programming language
Apache License 2.0
224 stars 11 forks source link

data kinds as an alternative to type-classes #442

Open johnynek opened 4 years ago

johnynek commented 4 years ago

The reason we can't implement universal equality and comparison is that we could have embedded functions (and external types) that we don't know how to compare. If we only had structs/enums recursed, we can do naive comparison, equality, serialization, etc...

We could introduce a kind system that understands data. So, you can have some type T <: * means T is a type that produces values, or list List <: * -> * given a type we can produce a List of that type which can hold values, but we could also have written: List <: \x -> x so, if we have a List[a -> b] we don't have a type type, but if we have List[Bool] we do have a data type.

Some types are \x -> *, e.g. struct Foo(input: a, fn: a -> Int) no matter what a is, this is not a data type.

Then we could possibly introduce functions like:

def operator ==[a <: Data](left: a, right: a) -> Bool:

A downside to this is that it isn't clear how we could leverage a <: Data programmatically. It could be a marker for compiler generated code (like equals, comparison, serialization, etc...)

avibryant commented 4 years ago

I don't entirely understand the notation/syntax here, but I really like the general idea of distinguishing between pure-data values and those mixed with functions and external references. Seems like a very broadly applicable distinction.

johnynek commented 4 years ago

yeah, I was thinking about a data-flow backend for bosatsu. It would be really nice to say you Collection[a <: Data] or something. you can't put functions into distributed collections.

If you had that limitation, the compiler could just generate serializers at compile time without the user needing to care about that.

avibryant commented 4 years ago

This is a bigger change than you're looking for, but: what if a in a generic type definition always refers to a data-only type, and you have to specify \x -> a if you want a function? (As I've described this, it would not be possible to be generic over both data-only types and functions).

Strictly less expressive, but also much simpler syntax, and making everything data-only by default I think would yield a lot of dividends.

johnynek commented 3 years ago

https://without.boats/blog/revisiting-a-smaller-rust/

That blog post suggests another kind: resource. A resource might be linearly typed which allows you to make it clear that only one owner for any resource at a time. Even in a functional language, this can be useful.