3 ms·

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

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 https://graydon2.dreamwidth.org/253769.html

zesterer 4y ago
> 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.

zesterer 4y ago

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