jinko-core / jinko

Jinko is a small and safe interpreted language with fast Rust and C FFI
GNU General Public License v2.0
32 stars 6 forks source link

Allow specifying a multi type's type to help with type widening ambiguities #643

Open CohenArthur opened 9 months ago

CohenArthur commented 9 months ago

e.g. with the following result type:

type Result[T, E] = T | E;

func ambiguous() -> Result[int, int] {
    15 // Ok or Err?
}

which we could instead write as:

type Result[T, E] = T | E;

func ambiguous() -> Result[int, int] {
    Result.T(15) // Ok
}

and with more descriptive generic names

type Result[Ok, Err] = Ok | Err;

func ambiguous() -> Result[int, int] {
    Result.Ok(15)
}
CohenArthur commented 9 months ago

this means that flattening ambiguities in the typechecker would now be allowed, which I'm not a big fan of. so this is more of a design question than an actual "let's do this" issue. does it even make sense for a multi type/sum type to have duplicated types?

CohenArthur commented 8 months ago

I think overall it would be better to have helps around designing sum types. the above problem can be avoided by creating a sum type instead of an union type, like so:

type Ok[T](T);
type Err[E](E);

type Result[T, E] = Ok[T] | Err[E];

which then allows Result[int, int] and requires disambiguation when returning the value:

func no_longer_ambiguous() -> Result[int, int] {
    Ok(15) // or Err(15)
}
CohenArthur commented 8 months ago

so having a shorthand for creating these types in the same scope would work well:

type Result[T, E] = type Ok[T](T) | type Err[E](E); // maybe? very verbose

we can have the kind system extend it and make it easier but it's even harder to read IMO:

type Result[T, E] = newtype["Ok", T] | newtype["Err", E];
CohenArthur commented 8 months ago

so probably it would be better to have Maybe be defined as a "sum type" as well -

type Just[T](T);
type Nothing;

type Maybe[T] = Just[T] | Nothing;

which could be different from something like Nullable[T]:

type Null;

type Nullable[T] = T | Null;

which would not allow a Nullable[Null] to exist