bosatsu icon indicating copy to clipboard operation
bosatsu copied to clipboard

data kinds as an alternative to type-classes

Open johnynek opened this issue 5 years ago • 4 comments

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...)

johnynek avatar Dec 04 '19 19:12 johnynek

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.

avibryant avatar Dec 05 '19 04:12 avibryant

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.

johnynek avatar Dec 05 '19 05:12 johnynek

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.

avibryant avatar Dec 05 '19 05:12 avibryant

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.

johnynek avatar Oct 02 '20 00:10 johnynek