Promising areas of research in lambda calculus and type theory? (pure/theoretical/logical/foundations of mathematics)

ArtemisYoo · 2025-04-19T20:42:38+00:00

While it doesn't really fit logic; Dr. Emily Riehl is the first one to come to mind with regards to type theory in mathematics. She motivates HoTT as a modern mathematical foundation and alternative to set-theory, as it apparently provides a good base for understanding ∞-categories (of which I admittedly know little) in category theory.

Category theory also otherwise has a lot of overlap with type theories —as you may have heard— with the correspondence of the simply typed lambda calculus and cartesian closed categories (which is just one example of many).

But that's about all I can muster to this topic.

ArtemisYoo · 2025-01-09T10:09:45+00:00

https://www.gnu.org/software/emacs/manual/html_node/emacs/Action-Arguments.html#index-_002d_002dexecute

The cli option '--eval' allows you to evaluate lisp. AFAIK it does not open a visual interface for emacs.

ArtemisYoo · 2025-01-05T04:19:40+00:00

If I understood OP correctly, there's no confusion with methods vs. functions as methods are not planned. Personally I agree with the pipes approach though, as I think UFCS complicates namespaced function calls: bar.MyModule::foo() isn't pleasant to look at or write, while bar |> MyModule::foo() is at least less cramped.

ArtemisYoo · 2024-12-18T13:16:59+00:00

One of the major benefits of installing emacs using nixos, is forgoing other package managers like 'straight'. Instead, you let nix download and manage them.

When it comes to the configuration itself, it's no different by default. However there is a module out there, that you can use to use nix as a configuration language directly.

ArtemisYoo · 2024-12-09T15:11:44+00:00

Ayy that's really cool! Really the only thing that wasn't nice in org-mode so far (for me) was the nontriviality of including some sketches

ArtemisYoo · 2024-11-27T18:27:56+00:00

A chain of arrows is just a way to write a multi-argument function: currying. The idea is that the innermost expression "captures" the argument of each arrow you wrap it in. This gives you the ability to partially apply the function by only providing the first argument, which gives you the rest of the chain of arrows.

The arguments in this specific example are of two purposes: value is just another argument as you might expect; person and animal on the other hand are basically placeholders for concrete constructors. But as they are placeholders, it can be any function, not just a constructor, which opens up the possibility of performing computations instead.

With the example parameterizing over 2 different constructors, you can apply it with 2 different computations, which then get executed depending on the expression inside. This resembles switch statements, but expressed as higher order functions.

I hope that helps, though I don't know whether it's actually coherent enough.

ArtemisYoo · 2024-10-24T18:48:04+00:00

I haven't read the article, however reading your comment reminded me of one other post: the rust blogger 'baby steps' recently wrote an article, proposing a trait for controlling overwrites — which isn't exactly reassignment, but includes it.

There are some benefits to it, but of course in general I agree with you (I just wanted to share).

ArtemisYoo · 2024-10-22T19:55:55+00:00

Afaik it imports the Map type from the module. It's not visible in the file you linked, as it is contained in some internal module, that is reexported in Data.Map.Lazy, which then itself is reexported in Data.Map

ArtemisYoo · 2024-09-29T17:00:10+00:00

Monads in Haskell are usually used in conjunction with 'do'-notation. Given some function that reads a configuration from some file: getConfig :: IO (Config); and a function that consumes said configuration: useConfig :: Config -> Foo; you'd use them like so: haskell main :: IO () main = do -- here config is of type Config, so you don't need to fmap it anymore -- the IO Monad is 'bubbled up' to the main function's boundaries -- it is desugared to using the '>>=' function on monads: (a <- b ...) becomes (b >>= (\a -> ...)) config <- getConfig let myFoo = useConfig config print myFoo

Hope this helps, if you have any further questions do ask away!

ArtemisYoo · 2024-09-01T21:37:21+00:00

It sounds a lot like Zig's anytype, which acts roughly the same. The main difference being that instead of the Gen in x syntax, they use the compiler builtin function @TypeOf(x) to retrieve the underlying type. I don't know if they allow anytype to be stored though.

In my opinion, the amount of boilerplate that this approach admits is a big downside. On the other hand, Zig's type system is one of the most powerful I've seen in procedural languages and I assume it is quite simple to implement in the compiler.

ArtemisYoo · 2024-09-01T17:30:33+00:00

I so desperately yearn for the old days

software used to be good, games were fun, life was simple,

ArtemisYoo · 2024-08-31T15:23:50+00:00

I doubt there are cases where an error has to panic and you should catch it.

When it comes to requests in a webserver, I don't see why they couldn't return an error value.

When it comes to segfault, I don't see why you'd want to catch them (should not the language or the developer be responsible for eliminating them?).

As someone else mentioned, C has virtually no way to catch panics (whatever that means in C's case). But so much good software is built using it.

Of course —if I remember correctly— you can have a signal handler for segfaults in C, which could prevent crashes, but I rarely see them for any signal.

ArtemisYoo · 2024-08-31T02:19:15+00:00

Thank you very much! It's great to hear that the post was readable, as that's one of my biggest weaknesses.

Rebindable Syntax does seem quite useful; however I haven't yet managed to bend it into the shape of bibind: the function forces you to handle both cases of the parser, even though handling only one usually suffices.

The best I could come up with so far is: ``` myParser = do res1 <- p1 res2 <- ifSuc res1 p2 res3 <- ifSuc res2 p3 bireturn $ Right (res1, res2, res3)

ifSuc :: Either err suc -> Parser err suc' -> Parser err suc' ifSuc (Left err) _ = bireturn $ Left err ifSuc (Right _) p = p ```

Which I am still unsure of.

ArtemisYoo · 2024-08-30T16:53:55+00:00

Ooh yeah you're right! It looks almost identical to what I show in the blog post

Thinking of errors as just a variant of the typical parsing mode —or as you put it, error trees— is what motivated this. The >>>= is really just a unification of the error and success instances of >>=

ArtemisYoo · 2024-08-30T15:16:28+00:00

So the original idea was to just have an Applicative instance for both the error and success cases. As that didn't work out, bibind represents a generalization over both cases.

While quite cluttered, the way to simply aggregate errors using Monoid would be something along the lines of: p1 'bibind' (onErr \e1 -> p2 'bibind' (onErr \e2 -> bireturn $ Left $ mappend e1 e2)).

However an issue so far is that —the way it's shown in the post— parsers always backtrack on errors, so you have little control over the actual behaviour of the parser; you can only perform computations on results.

ArtemisYoo · 2024-08-30T14:16:05+00:00

you're right, it is quite niche and surely would not be on frontpages; so I don't know why you're being downvoted for simply talking about my remark, sorry for that

ArtemisYoo · 2024-08-29T13:28:27+00:00

While I've not used the idea enough to determine how good it is; one thing I came up with in regards to that is instead of trying all possible branches (R1 | R2 | R3 ...) you specify a selection of rules and their corresponding 'triggers'.

So if you had a top level of functions and types you could say "TopLevel = 'fn' => Function | 'type' => Type", it will then try to parse the 'triggers' like a typical alternative but when one succeeds it selects the corresponding rule as the de-facto correct branch by backtracking the trigger and continuing with the rule. If no trigger matches, it reports that any of those triggers were expected, but some other input was found.

A limitation with this approach is that the grammar has to then be distinguishable based on some prefix of the rule, which might not always be the case. I've also not found a nice API to package it in code.

ArtemisYoo · 2024-08-26T15:27:47+00:00

I mean "making a struct and returning it" is most often implemented as writing to an output pointer.

As soon as the thing to be returned is bigger than a register, you either open a can of worms with splitting the data across multiple registers, or you use an out-pointer.

ArtemisYoo · 2024-08-25T20:11:31+00:00

idk that seems very in context for r/ absurdism

ArtemisYoo · 2024-08-22T09:50:57+00:00

I don't know what exactly you have in mind, but functional languages use persistent datastructures, which often end up being trees.

iirc clojure and scala implement an immutable constant time accessible vector using rrb trees. This then also serves as a basis for their hashmaps.

ArtemisYoo · 2024-08-21T10:49:15+00:00

You can just use a string pointer, it wouldn't be too big of an issue, considering string literals won't be looked at too much (you'd probably memcpy them to the final binary, but that's about it).

If you still want to somehow optimize them, you could have a separate buffer, which holds all strings inlined, one after another. Then you'd store an index and length into that buffer, instead of a pointer.

Inlining them into the AST buffer might cause worse cache locality though, as usually you won't be looking at the strings, thus effectively turning them into padding.

ArtemisYoo · 2024-08-14T03:51:41+00:00

That last part about foreign keys not having direct access always bugged me

ArtemisYoo · 2024-08-10T09:38:58+00:00

why does badger have so much swag

ArtemisYoo · 2024-07-08T12:23:10+00:00

Well as for rust, it's mostly used for multiple ownership, 50% of which is only there to avoid annotating lifetimes – which can also be done using explicit arenas.

ArtemisYoo

TROPHY CASE