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