4 ms·

> 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 m

> 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.tao#L14-L21 https://github.com/zesterer/tao/blob/master/examples/debug.t...)

skavi 4y ago
would you mind explaining the linked code?
- zesterer 4y ago
  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/Prelude.html#v: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.

skavi 4y ago

would you mind explaining the linked code?

zesterer 4y ago
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/Prelude.html#v: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.