Very cool! This might be a naive question. Are your arithmetic patterns equivalent to dependent types, like those found in Idris?
Tao: A statically-typed functional language
11–20 of 98 posts
Re: Tao: A statically-typed functional language
#12So is the language planned to be computationally complete or total? I was not completely clear on your definition of totality. But I am all for not Turing-complete models of computation that still do useful things.
For now, just total (i.e: functions can't panic, throw exceptions, etc.). I'd like to explore termination analysis in the future though!
Re: Tao: A statically-typed functional language
#13Very cool! This might be a naive question. Are your arithmetic patterns equivalent to dependent types, like those found in Idris?
They're more akin to 'destructuring' natural numbers into successors. Consider:
data Nat = Zero | Succ Nat
You could pattern match on this Nat, fetching the inner Nat, allowing the type system to prove that all cases are handled exhaustively. Arithmetic patterns just extend this notion to the built-in Nat type.
Full dependent typing is something I'd like to experiment with in time, but I'm not there yet.
Re: Tao: A statically-typed functional language
#14A few observations: Seems very ML/Haskell inspired. All tuples seem to require parenthesis. Definitely not ergonomic on a qwertz layout (Altough, what language is?) No current plans for an interactive/repl version it seems No dependant types either. Overall, pretty interesting. Definitely warrants a closer look.
Pretty much!
The language does support limited sugar for tuples without parentheses in some specific cases, such as `match` and `let`:
let x, y = 5, 4 in
...
match x, y in
| 4, 7 => None
\ _, y => Just y
Re: Tao: A statically-typed functional language
#15So is the language planned to be computationally complete or total? I was not completely clear on your definition of totality. But I am all for not Turing-complete models of computation that still do useful things.
For now, just total (i.e: functions can't panic, throw exceptions, etc.). I'd like to explore termination analysis in the future though!
It's an unfortunate conflation between total functions and total functional programming, which is done with non-terminating languages. If I'm reading you right, Tao currently requires functions to be total but is not designed to always terminate.
Re: Tao: A statically-typed functional language
#16I don't understand what the possible use case for using a \ for the final bar for sum types would be. It would just make it a diff to add a new item at the end. I was hoping it had Unicode support looking at the example screenshot, but no, it's just a ligature font confusing users.
Tao isn't indentation-sensitive, so nested `match` expressions are ambiguous without the trailing \ branch. I don't know whether I'll keep this syntax though. I'm increasingly wondering whether it's better to just bite the bullet and go all in with indentation sensitivity. That said, the existing \ syntax can be quite nice to read: https://github.com/zesterer/tao/blob/master/lib/parse.tao#L5...
Why not just require parents for nested cases? IMO this is fairly unambiguous, even to people unfamiliar with a particular language.
Re: Tao: A statically-typed functional language
#17Earlier quoted context omitted.
For now, just total (i.e: functions can't panic, throw exceptions, etc.). I'd like to explore termination analysis in the future though!
It's an unfortunate conflation between total functions and total functional programming , which is done with non-terminating languages. If I'm reading you right, Tao currently requires functions to be total but is not designed to always terminate.
Yes. This is something I've been thinking about a lot, as it happens! In particular, one of the great benefits of pure languages from an optimisation standpoint is that unused values can always be optimised away, but this is not the case if we treat termination (or non-termination) as a side effect! For now, I'm treating it as not being a side-effect (as does C++, although C++ goes a step further and treats it as straight-up UB in certain conditions). This is something I've still yet to nail down semantically.
Re: Tao: A statically-typed functional language
#18A few observations: Seems very ML/Haskell inspired. All tuples seem to require parenthesis. Definitely not ergonomic on a qwertz layout (Altough, what language is?) No current plans for an interactive/repl version it seems No dependant types either. Overall, pretty interesting. Definitely warrants a closer look.
Pretty much! The language does support limited sugar for tuples without parentheses in some specific cases, such as `match` and `let`: let x, y = 5, 4 in ... match x, y in | 4, 7 => None \ _, y => Just y However, these cases only incidentally lower to tuple pattern matching, and deliberately hide the fact that tuples are used internally.
Are you planning on having something similar to computation expressions? Altough, I guess thats basically covered within the do notation.
https://docs.microsoft.com/en-us/dotnet/fsharp/language-refe...
Re: Tao: A statically-typed functional language
#19Hardly ever is "good REPL" one of the features of these new languages. Do they think it's irrelevant or is making such a thing too difficult compared to all these more CSy features?
REPLs are often difficult to reconcile with AoT compilation and static analysis, particularly in the context of things like type inference (at least, in a way that preserves semantics). It's on my mental todo list, but not a priority for me.
How fast is the compiler? In many cases a report can just be syntactic sugar for compiling and running an accumulating log of source code lines. It’s not really important how it works under the hood as long as it’s mostly transparent to the user.
As a side effect, it might also be a good way to keep your compile times down.
Re: Tao: A statically-typed functional language
#20Sorry, what's that font in the github screenshots?