[landonxjames]

Came across this post [0] by Graydon Hoare (original author of Rust and member of the Swift team) in an HN comment the other day. Lots of interesting discussion about future paths for language design work, including some discussion of Effects Systems.

Curious how Tao is pushing the limits on that front?

[0] https://graydon2.dreamwidth.org/253769.html

[zesterer]

> Curious how Tao is pushing the limits on that front?

I don't want to put emphasis on "pushing the limits" because I'm still very new to language design and mostly self-taught. There are bigger and better languages pushing the envelope further than Tao!

That said, I've been experimenting with:

- Expressing totality and type inhabitance in the type system

- Effect systems (including user-defined effects, effect handling, parametric effects, lowering to monadic IO, etc.)

- Typeclass inference via typeclass variables (Tao can handle several cases that are ambiguous even in Rust, such as the following: https://github.com/zesterer/tao/blob/master/examples/debug.t...)

[skavi]

would you mind explaining the linked code?

[zesterer]

The code is a bit of a gimmick, not really the sort of thing you'd have in a real program. It's just there to demonstrate that the compiler doesn't need explicitly telling which typeclasses associated types correspond to. That said:

    fn show_negative A : A -> Str where
        A < Neg,
        A.Output < Neg,
        A.Output.Output < Neg,
        A.Output.Output.Output < Neg,
        A.Output.Output.Output.Output < Show,
    =
        a => (----a)->show

This is a function, called `show_negative`, that is generic over a type, `A`. The function takes an instance of `A` and returns a `Str` (string).

In terms of implementation, the function is quite simple: it just negates the input value a bunch of time and then `show`s it as a string using the `Show` typeclass (equivalent to Haskell's `show`: https://hackage.haskell.org/package/base-4.16.1.0/docs/Prelu...).

Arithmetic operations such as negation are defined using typeclasses. Here's the definition of `Neg`:

    class Neg =
        => Output
        => neg : Self -> Self.Output

This means that types that can be negated must provide two things: an output type produced when they're negated, and a function that actually performs the negation. For example, `Nat` (natural number) looks like:

    member Nat of Neg =
        => Output = Int
        => neg = fn x => (implementation omitted because it's a built-in intrinsic)

i.e: when you negate a `Nat`, you get an `Int`.

The `where` clauses on the `show_negative` just constrains the output type of negating the `A` in such a way that its output type is also constrained, in a chain, with the final type in the chain being `show`-able.