introit

The Yatima Standard Library (by lurk-lab)

Introit Alternatives

Similar projects and alternatives to introit

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a better introit alternative or higher similarity.

introit reviews and mentions

Posts with mentions or reviews of introit. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2021-06-07.
  • Yatima: A programming language for the decentralized web
    16 projects | news.ycombinator.com | 7 Jun 2021
    I would dearly love to make Yatima a usable theorem prover, and Lean has been a huge inspiration particularly regarding syntax. But building a usable theorem prover is a huge project, and at minimum will require substantial work on our theory, on type-inference (which is fairly minimal right now) and on advanced features like quotient types or univalence.

    On that point, we've done a little exploration on encoding the Path types from Cubical Type Theory as self-types, and I think there's some promising work to be done there. But I know my limits and while I feel very comfortable building a useful programming language that can do a little bit of basic theorem proving, I know that doing a proper job on a real theorem is going to require larger scale resources.

    As far as the link from the Self-Types paper, our theory is similar to their System S, but is not the same. Not 100% sure but I think the main relevant difference here is about Leibniz equality, which iirc allows for saying `a == b` when `a` and `b` are of different types. Yatima's Equal type https://github.com/yatima-inc/introit/blob/main/Equal.ya, implements the more standard homogenous/Martin-Löf equality, but this is just a library, not a language builtin.

    We really do need to write an actual paper for Yatima's theory though, especially considering that we've combined the self-types from System S with a variation of Quantitative Types a la Idris 2. Writing that paper is likely step 0 of any Yatima as a theorem prover project, until then we should view Yatima as just an unsound functional programming language with some nice type-level features

    16 projects | news.ycombinator.com | 7 Jun 2021
    Sure, thanks for the feedback. Our standard library is here: https://github.com/yatima-inc/introit, I'll edit the README to make that more prominent

    As far as docs and tutorials, we weren't planning on doing a public release for another month or two, so there isn't anything yet. The language is still pre-alpha, so our focus has been on getting the core working correctly before smoothing the on-ramp.

    Also, tbh, I'm not 100% settled on what the user-facing syntax should be. Right now we have a simple lisp-like core syntax, but I'm thinking about implementing something like Racket's #lang declaration to allow the user to define and import frontends to that core syntax.

    16 projects | news.ycombinator.com | 7 Jun 2021
    Their explanation is reductive, but it looks like more than that. For example, in the standard library [0] the definition of the Map type is a function of other types.

    [0]: https://github.com/yatima-inc/introit/blob/main/Map.ya#L10

    16 projects | news.ycombinator.com | 7 Jun 2021
  • A note from our sponsor - Onboard AI
    app.getonboardai.com | 22 Feb 2024
    Onboard AI learns any GitHub repo in minutes and lets you chat with it to locate functionality, understand different parts, and generate new code. Use it for free at app.getonboardai.com. Learn more →

Stats

Basic introit repo stats
5
20
2.6
2 months ago

lurk-lab/introit is an open source project licensed under MIT License which is an OSI approved license.

The primary programming language of introit is Nix.

Power Real-Time Data Analytics at Scale
Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
www.influxdata.com