[HN Gopher] Tao: A statically-typed functional language
___________________________________________________________________
Tao: A statically-typed functional language
Author : memorable
Score : 214 points
Date : 2022-07-04 14:11 UTC (1 days ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| tm-guimaraes wrote:
| The promises are great, but will it deliver? It's seems the
| language has a really huge scope with lots of hard problems to
| solve.
|
| The thing I loved about golang was that it's just "good enough"
| in lots of areas instead of being the best or perfect. That
| allowed more time ti works on other parts of an ecosystem.
|
| But since Tao is an hobby project, i just hope the author goes
| nuts and enjoy working on all those things. It is indeed a cool
| lang.
| zesterer wrote:
| I am indeed "going nuts"!
|
| As mentioned in the README, I don't see Tao as a production-
| quality language (at least, for the foreseeable future). I'll
| leave that to the experts. Instead, I'm more interested in
| exploring the limits of new language design ideas (effect
| systems in particular). There are already a few interesting
| things Tao does that I've not seen elsewhere.
| landonxjames wrote:
| 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 wrote:
| > 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/mast
| er/examples/debug.t...)
| skavi wrote:
| would you mind explaining the linked code?
| zesterer wrote:
| 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.
| LelouBil wrote:
| A couple of months agow I had never tried functional programming
| languages. Having learned Rust in the past year (and loving it )
| made me want to try out Haskell since I always wondered about
| functional languages and I likes Rust's strong type system.
|
| I go a bit dissappointed with Haskell, but right now I'm reading
| Tao's README and this looks like everything I've ever wanted !
| I'm gonna try it out right now.
| throwaway17_17 wrote:
| Can you expand on what disappointed you about Haskell. I'm not
| looking to convert you or anything, just curious.
| okasaki wrote:
| Sorry, what's that font in the github screenshots?
| zesterer wrote:
| Iosevka Fixed Slab Semibold
| kortex wrote:
| Nice work! Looks super interesting and rewarding to work on.
|
| Is the namesake "tao" meaning "the way"? Or perchance a nod to
| Terry Tao?
| zesterer wrote:
| > Tao or Dao is the natural order of the universe whose
| character one's intuition must discern to realize the potential
| for individual wisdom
|
| It echoes how I feel when I write programs in languages with
| strong static type systems: that of the compiler almost
| fatalistically leading me towards a solution that naturally
| fits the problem space. A metaphor I like to use is that of an
| artist knocking away pieces of marble to reveal the statue that
| was always there beneath.
|
| And, yes, it's great fun to work on! Everybody should give
| writing a compiler and designing a language a try!
| pjmlp wrote:
| I guess not to mix with Tao, next gen OS for Amiga, based on
| bytecode as distribution format.
|
| https://www.edn.com/amiga-reborn-via-tao-alliance/
| lloydatkinson wrote:
| Somewhat familiar with FP and enjoy some of its benefits in my
| projects but I haven't really used a full blown FP language like
| Haskell. What exactly is a type class? I haven't found an
| explanation that makes a lot of sense to me. I think at one time
| I believed them to be some kind of contract like an interface in
| a OO language.
|
| Can someone explain?
| zesterer wrote:
| A typeclass (or in Rust, a trait) is something that describes a
| set of behaviours that must be implemented by a type (in OOP
| languages, abstract classes are broadly equivalent).
|
| For example, the typeclass `Eq` describes how values of a type
| might be compared for equality. class Eq =
| => eq : Self -> Self -> Bool
|
| The typeclass requires that types conforming to it provide a
| function, `eq`, that takes two instances of itself and returns
| a bool (indicating whether the instances are equal). And member
| of this typeclass might look like: for A, B
| member (A, B) of Eq where A < Eq, B <
| Eq, = => eq = fn (a0, b0), (b0, b1) => a0
| == a1 && b0 == b1
|
| You can read this as "for any two types, A and B, a tuple of
| both can also be compared for equality provided both A and B
| can themselves be compared for equality"
|
| Typeclasses become useful because they allow you to constrain
| generic type parameters. For example, we can now write a
| function that determines whether a list contains a matching
| value: fn contains A : A -> [A] -> Bool where
| A < Eq, = | _, [] => False \ k,
| [x .. xs] => x == k || xs->contains(k)
|
| All of this is checked at compile-time by the compiler,
| ensuring that the function can only be called with types that
| can be compared for equality.
| lmm wrote:
| One of the things that's hard to follow is that people conflate
| typeclasses and typeclass instances.
|
| So, the typeclass itself is like an interface, but rather than
| having classes that implement that interface directly, you have
| typeclass instances which are like an adapter between a value
| (struct) and the interface - or like a virtual function table.
| You know how a class instance is essentially a struct + a
| (pointer to a) virtual function table? Imagine making those two
| pieces more distinct in code - the typeclass instance is the
| stanadlone virtual function table.
|
| So your object state is more exposed - you can't really have
| private fields in this paradigm since your state is just a
| struct value. But it's clearer what's what, and it's much
| easier to adapt types to interfaces even when the authors
| didn't know about each other, since the typeclass instance can
| be defined separately from both the typeclass and the value
| type (although there are possible inference problems with
| this). So lots of secondary cross-cutting functionality
| problems where OO languages tend to end up with an ad-hoc type
| registry (e.g. serialization or database mapping - just look at
| what projects like jackson-datatype-joda or joda-time-hibernate
| have to do to get themselves registered) are easier to solve in
| this model.
| galaxyLogic wrote:
| What about OOP classes and inheritance? Data hiding? Modules?
| zesterer wrote:
| Tao has typeclasses (like Haskell) that allow for compositional
| parameteric polymorphism. It also has data types (records, sum
| types, etc.) and functions, but deliberately does not bundle
| the two together.
|
| There is no module system yet (only a temporary C-like #include
| system): that's on my list of things to work on!
| toastal wrote:
| I 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.
| zesterer wrote:
| 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...
| ratww wrote:
| The \ syntax is my favorite part so far, I'm definitely gonna
| copy it for my toy language, hope that's ok ;)
| zesterer wrote:
| Go for it! IIRC it was suggested by someone else in the
| #langdev channel on the Rust Community Discord, so I can't
| claim to own the idea.
| catlifeonmars wrote:
| Why not just require parents for nested cases? IMO this is
| fairly unambiguous, even to people unfamiliar with a
| particular language.
| zesterer wrote:
| In a previous revision of the language, I did!
| (https://github.com/zesterer/tao/tree/old). I decided
| against it because, in short, I find the trailing
| delimiters to be quite ugly.
|
| Because this is purely a personal project, I'm thankfully
| not constrained by such mundane concerns as "ergonomics"
| (unless such concerns relate to me while I'm working with
| it). I think Pythonic syntax is probably the way to go
| long-term though...
| patrickkidger wrote:
| Personally I'm a big fan of Julia's syntax here.
| Indentation-insensitive with the use of the word "end" as
| the terminator for all types of block. In practice you
| can lay it out like Python, and the "end"s help you keep
| track when e.g. you need to place a single expression
| after some deeply-nested blocks.
| solatic wrote:
| > Totality
|
| Best of luck. Dhall is a current language with totality, but it
| runs into impossibly high memory requirements as a result. We had
| CI workers with 16 GB RAM run into out-of-memory issues because
| of the sheer size of the totally expanded type space (sum types
| of types which are themselves sum types of types which are
| themselves sum types etc... Exponential growth is easy).
|
| I appreciate that this is scoped as a hobby project for now, not
| recommended for production, so like I said, best of luck :)
| atennapel wrote:
| I'm not sure what you mean with totally expanded type space.
| But it sounds like Dhall has an issue with
| unfolding/normalisation.
|
| Totality shouldn't have any special impact on memory usage as
| far as I know. It just restricts the kind of recursive
| functions and data types you can write.
| iamwil wrote:
| What were the series of resources or readings that you did to
| help you create Tao?
| zesterer wrote:
| There wasn't really any single resource I read. Frustratingly,
| I find it quite difficult to read research papers (I'm told
| it's a skill acquired with practice, but it's something I've
| never gotten into). Most of the implementation is the product
| of several rewrites and false-starts, along with the occasional
| hint I've read about here or there on the web.
| darthrupert wrote:
| Hardly 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?
| zesterer wrote:
| 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.
| pohl wrote:
| Do you suppose that might be an outmoded historical bias? I'm
| wondering if maybe the advancement of hardware has made it so
| that the costs of AOT compilation and a type system should no
| longer stand in the way of delivering a reasonable REPL
| experience. Swift's "playgrounds" seems to do alright -- a
| real outlier in this regard.
| skavi wrote:
| Haskell has a REPL. No idea whether it's considered good
| though.
| catlifeonmars wrote:
| 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.
| substation13 wrote:
| What if one of those lines fires the missiles?
| zesterer wrote:
| Fast enough for this approach to work for small examples.
| For longer examples, I'm less confident: I've yet to
| implement a proper module system (other than a slightly
| more principled version of C's #include) so this currently
| means compiling the entire standard library on every REPL
| line. Thankfully, the compiler can still handle this within
| about 100 milliseconds on my machine. Perhaps when I have a
| more rugged module system I can look into this more, thanks
| for the suggestion!
| darthrupert wrote:
| That's not even close to being adequate for the kinds of
| things good REPLs are good for.
| shirogane86x wrote:
| This looks great! I've actually been experimenting with making a
| functional language too, in rust - so I'm probably gonna read
| through the code soon! Also, those error messages look really
| good - I'm totally gonna try ariadne and chumsky out :)
| zesterer wrote:
| Good luck! Feel free to open a discussion topic or issue if you
| have any questions!
| throwaway17_17 wrote:
| Since someone brought it up, and since I don't speak rust...
| are the error message formats (i.e. the lines and crossings)
| made by a rust library or did you implement them? They are
| certainly visually nice.
| zesterer wrote:
| They are made by a Rust library, but it's a library I wrote
| for this project (now used by others too):
| https://github.com/zesterer/ariadne
| magicalhippo wrote:
| Great readme, and definitely made me want to play with it. I was
| raised on procedural programming and never really got into proper
| functional programming, but somehow this just clicked for me.
| erezsh wrote:
| Asking as a complete newbie in this paradigm, but what's the
| benefit of writing factorial like this? fn
| factorial = | 0 => 1 \ y ~ x + 1 => y *
| factorial(x)
|
| Instead of | y => y * factorial(y-1)?
| zesterer wrote:
| Subtraction of natural numbers is non-total, and can result in
| negative numbers, which cannot be represented as a natural
| number. Most languages throw an exception, panic, etc. None of
| these are solutions I'm happy with.
|
| In Tao, natural numbers don't support subtraction but you can
| decrement them by pattern-matching as in this example, allowing
| the compiler to 'check your workings' and statically prove that
| your program can never result in underflows.
|
| In a similar vein, you can't index directly into a list
| (because indexing is a fallible operation). Instead, you must
| pattern-match on the list and explicitly handle the empty case
| (you can also write a utility function to do this for you like
| so) fn nth : Nat -> [A] -> Maybe A =
| | _, [] => None | 0, [x ..] => Just x \
| n + 1, [.. tail] => tail->nth(n)
|
| Used like: [1, 2, 3]->nth(1) # Evaluates to
| `Some 2`
| Akronymus wrote:
| A 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.
| zesterer wrote:
| 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.
| Akronymus wrote:
| 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...
| zesterer wrote:
| Yes! As you say, the do notation + monads covers this, but
| I'm planning to remove it in favour of a slightly more
| general 'effect basin' syntax that I'm currently working on
| (syntactically similar to Rust's async + await, but
| generalised to all effectful operations like mutation, IO,
| etc.). Example here: https://github.com/zesterer/tao/blob/m
| aster/examples/mutate....
| platz wrote:
| > No dependant types either.
|
| You're funny
| Akronymus wrote:
| How so? I personally find dependant types to be very
| interesting, but I get that they are a PITA to implement. So,
| for me, it was simply an observation that there are currently
| no plans for dependant types. No value judgement intended.
| isaacimagine wrote:
| Not to be pendantic, but I think you made a joke without
| realizing it.
| Akronymus wrote:
| I did? I have now spent like 20 minutes trying to figure
| it out. But I still don't get it.
| macintux wrote:
| I'm guessing it has something to do with the keyword
| "either" and Haskell types, but I'm otherwise clueless.
| Every time I look at Haskell I run the other way.
| zesterer wrote:
| I think it was "value judgement" (dependent types allow
| dispatching over a value in the type system)
| maweki wrote:
| So 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.
| zesterer wrote:
| For now, just total (i.e: functions can't panic, throw
| exceptions, etc.). I'd like to explore termination analysis in
| the future though!
| samatman wrote:
| 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.
| zesterer wrote:
| 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.
| zesterer wrote:
| Hey, author here. I definitely didn't expect to see Tao on Hacker
| News. As is probably obvious, the language is _extremely_ early
| in its life, and it 's not practical to write anything but
| trivial examples in it yet. Please don't judge!
| agumonkey wrote:
| good luck
| code_biologist wrote:
| I remember a golden age of programming reddit and HN in the
| late 2000s that inspired me learn a bunch of new programming
| languages, Haskell the biggest influence among them. It seemed
| like people were always posting their own personal languages,
| lisps (I remember the hot takes on Arc lol), and such all the
| time. I have very fond memories of going through Jack
| Crenshaw's "Let's Build a Compiler" after seeing it posted a
| bunch of times, then trying to build my own language in a
| similar vein.
|
| Cheers to you, and I hope you're learning and having fun
| working on your project!
| zesterer wrote:
| Thanks!
| jrumbut wrote:
| I too remember that time and it left me terribly jaded
| about the utility of new languages.
|
| This is the first I've seen in a while where I think the
| offering hits a spot on the tradeoff continuum that is
| distinctive and where I can picture many circumstances
| where I would want to use this language (the soundness
| aspect is a big part of that).
| dmix wrote:
| Nice work on the README. Gets right to the point about what it
| look likes and what the goals are.
| yccs27 wrote:
| Tao looks super cool, and similar to the kind of language I'd
| personally make if I decided to create one. Kudos for actually
| implementing yours!
|
| Some specific questions about the language design: - Does your
| flavor of algebraic effects allow distinct effects of the same
| type (e.g. two separate int-valued `State`s)? I haven't seen
| anyone talk about this, but it seems like a potential problem
| with effects.
|
| - Do you have plans for making pattern matching extensible?
| I've thought a lot about how this could be possible with optics
| (the FP construction), but haven't found a nice solution yet.
| zesterer wrote:
| > Does your flavor of algebraic effects allow distinct
| effects of the same type
|
| Could you give an example of what you mean by this? Multiple
| effects can be combined together (although I'm still working
| on handlers for multiple effects), for example:
| effect console = input + print fn greet_user :
| console ~ () = { print("Please enter your
| name:")!; let name = input!;
| print("Hello, " ++ name)!; }
|
| > Do you have plans for making pattern matching extensible?
|
| I have no plans as of yet. Extensible pattern-matching seems
| to me to be quite hard to unify with exhaustivity. Tao
| supports most of the patterns that Rust/Haskell supports.
| throwaway17_17 wrote:
| I think GP is referring to having two effects, like State1
| and State2, both of which allow for stateful effects on int
| references, and then being able to handle the effects
| uniquely for each effect. I think the underlying type
| theoretical question would be are Tao's effects nominally
| vs. structurally typed.
|
| A more practical example would be having two state-like
| effects for use as different allocation/deallocation
| strategies.
| zesterer wrote:
| Tao's effects are nominally typed, so there's no way to
| accidentally mix them up in the way I assume you're
| describing. For example: # Define a new
| effect that yields to the caller effect yield A =
| A => () # A generator that emits numbers
| def one_two_three : yield Nat ~ () = {
| yield(1)!; yield(2)!; yield(3)!;
| } # Print the numbers to the console
| def main : io ~ () = { one_two_three
| handle yield Nat with n => print(n->show)! }
| roguas wrote:
| Designing a PL is a hard complicated process, very slim portion
| of professional programmers are able to deliver some novelty
| here. I think any judgement should be treated as merely a
| feedback on the usefulness of this language. The effort alone
| is exceptional accomplishment. Take care.
| zesterer wrote:
| Thanks for your kind words :)
| dataangel wrote:
| > A rather dogged and obnoxious opinion of mine is that the
| 'optimisation ceiling' for statically-typed, total functional
| programming languages is significantly higher than traditional
| imperative languages with comparably weak type systems.
|
| Curious about plans for this. When Haskell use exploded I
| followed a lot of the blogs talking about it someday being
| faster than C because purity made compiler reasoning easier and
| stream fusion and other things were going to change the world,
| but as time went on idiomatic Haskell never came even close to
| C. Now having a lot of performance experience I think a major
| factor is that functional languages insist on using lists for
| everything, which map poorly to hardware. Looking at your
| screenshots, it looks like it still employs the list paradigm.
| zesterer wrote:
| So... I want to preface this by saying that I'm very, very
| far from being an expert on this topic. Although Tao's
| compiler has a MIR optimiser, it only covers the basics
| (inlining, constant folding + symbolic execution, etc.).
|
| I think one of the main reasons that Haskell failed to solve
| this is actually the same reason that many lower level
| languages failed: it places too many requirements on data
| representation. In the case of C/C++ and even (to a lesser
| extent) modern languages like Rust and Swift, this is because
| they make promises about representation to the programmer
| that allow you to circumvent aspects of the language and
| still write correct code: be it transmutation, casting, field
| offsets, etc. In the case of Haskell, lists have an entirely
| arbitrary length and the language makes no effort to
| constrain this requirement in the type system, meaning that
| the compiler can only speculatively optimise a list into an
| unboxed array. In a language with dependent types, it should
| be possible to constrain the size of a list with the type
| system, allowing the optimiser to do its job without need for
| speculative whole-program analysis.
|
| The other reason Haskell doesn't quite succeed is
| monomorphisation (or lack thereof). Haskell's support for
| first-class higher-ranked types means that the language can't
| feasibly make promises about monomorphisation, and as a
| result it needs to revert to boxing and dynamic dispatch far
| more than it really should. Conversely, Tao is designed to
| monomorphise in all cases from the start.
|
| Rust demonstrates that functional programming (and in
| particular, programming with higher-order functions) is more
| than possible to optimise very well, and it does this by
| promising monomorphisation through the type system, allowing
| the compiler to aggressively perform static dispatch and
| inlining.
|
| From what I've seen, GHC also fails to pick a lot of low-
| hanging fruit. The last time I checked (perhaps this has
| since changed) GHC often struggles with things like TCO and
| inlining in relatively simple cases as a byproduct of its
| design (all functions are dynamically dispatched by default,
| with inlining being a speculative optimisation).
|
| I need to do a little more writing about exactly what ideas I
| have for Tao, but other languages of similar ilk demonstrate
| that Haskell is very far from the pinnacle of what is
| possible (for example, Koka's Perceus reference reuse:
| https://koka-lang.github.io/koka/doc/book.html#why-perceus).
| shadowofneptune wrote:
| > all functions are dynamically dispatched by default, with
| inlining being a speculative optimisation
|
| Could you please point me to other approaches to inlining?
| I am also working on a personal language and it could be
| helpful.
| zesterer wrote:
| Rust gives each closure a unique type (see the `Fn`
| trait: https://doc.rust-lang.org/core/ops/trait.Fn.html),
| allowing the compiler to always statically dispatch to
| the exact function body at compile-time. That said, this
| is a rather more explicit approach that won't necessarily
| fit everything.
| slavapestov wrote:
| I'm curious how you implement associated types and equivalences
| between them. In the most general case, this allows encoding an
| arbitrary finitely-presented monoid in the type system, and the
| word problem on finitely-presented monoids is undecidable.
| However, you mention your type checker is Turing-complete.
| zesterer wrote:
| Yep, this is the case: the type-checker allows arbitrary
| computation to occur at compilation time. You can see some of
| that here, where I've implemented peano
| arithmetic/addition/multiplication/branching using the type
| system:
| https://github.com/zesterer/tao/blob/master/examples/type-
| as... . I've not yet had the time or mental fortitude to
| implement something more non-trivial like N-queens or a
| Brainfuck interpreter, but perhaps eventually!
| slewis wrote:
| Very cool! This might be a naive question. Are your arithmetic
| patterns equivalent to dependent types, like those found in
| Idris?
| zesterer wrote:
| 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.
| schaefer wrote:
| The Tao that can be told is not the true Tao.
___________________________________________________________________
(page generated 2022-07-05 23:01 UTC)