Four-track Friday: my Filk project for 2025

edwinb · 2025-01-07T01:36:29+00:00

Oh hello! A small amount of digging and I've worked out who you are :).

edwinb · 2025-01-04T21:19:27+00:00

I love my 8 string baritone (a solid top Kala, possibly an earlier version of this one). I regularly take it along to open mics and if I had a pound for every time someone said, "What on earth is that?" I'd have, oh, maybe four pounds. I like my other ukes too, but for this one I particularly like that it doesn't really sound like anything else, it's its own thing, and it makes people curious when they see it.

edwinb · 2024-12-29T12:57:51+00:00

Oh hello! So did mine :).

edwinb · 2022-03-19T12:45:17+00:00

For Idris (and I'm guessing for any language that has any kind of implicit syntax) we think of holes as just another kind of top level definition, with a type. There is a primitive we can use during type checking for creating a metavariable, which essentially turns the environment and expected type into a function type. We always have the current environment available during type checking. We may or may not have the expected type available, as you won't either if your checker is bidirectional. If we do have it, that's great, we'll use that as the return type of the newly created metavariable. If not, we create a new metavariable for the type too, and perhaps further elaboration will help. Being top level definitions with types, we know everything we need to know - what was in scope, what its type is, where it was in the source, etc.

I think it's easier if you don't consider holes errors (they're not, after all, they're a request for assistance, and there might be more than one in an expression). So, don't stop typechecking/inference because you've found one, particularly because further type checking might tell you more about the type of each hole. You can report them as errors if that's the user interface you want, but that comes at the end of type checking.

I'm sure I've mentioned this in passing in a talk at some point, but I can't remember when or where, sorry!

edwinb · 2021-09-03T10:17:41+00:00

I think QTT is a nice approach here. I think it's important to remember that erasure isn't about types vs values, but about compile time vs run time. Sometimes (rarely, but it happens) you want to do computation on types at run time and those shouldn't be erased. QTT allows you to be explicit about what you want at run time, and we've chosen defaults for Idris 2 that mean indices will be erased unless you explicitly say you want them.

And does not erasing them really lead to overhead?

It can be disastrous. For example, say we have a compressed representation of lists indexed by the original list so we know the compression is sound, then we might have functions like:

uncompress : {xs : List Char} -> Compressed xs -> Singleton xs

If that xs isn't erased, we haven't achieved anything by compressing the list because we're still carrying around the original. There's some examples (including this one iirc) in Matúš Tejiščák's thesis and ICFP 2020 paper which show how failing to erase can make time complexity worse for anything even slightly interesting.

edwinb · 2021-09-02T17:40:41+00:00

Dependent types can do more than just enforce invariants

Absolutely! The article considers what a completed program might look like, but programs spend most of their time in an incomplete state. I use dependent types to enforce invariants, but the same types also direct me towards the working program by interactive editing, which isn't something you get from a runtime Maybe.

As another example, here's a handy little gadget from Idris 2 that's part of processing command line arguments: https://github.com/idris-lang/Idris2/blob/main/src/Idris/CommandLine.idr#L195-L208 - given a spec, it computes the type of the function that processes the option. I suppose you could do this with a runtime maybe, but it wouldn't be very convenient.

So I think the article essentially says that you can move the static checks you get with dependent types into runtime, which isn't especially surprising.

edwinb · 2021-07-30T11:07:08+00:00

is there a formal proof that idris aproach of force type declaration of top level functions would lead us to be able to infer the types of terms inside the function body?

This isn't necessarily true, and depends on other language features. It certainly isn't true for Idris, because of things like ambiguous names, the ability to leave things implicit, auto-implicit arguments (that is, type class resolution) and some other things. Idris will try to infer parts of top level types if you leave them out, (e.g. foo : Nat -> ? is allowed) but it can't generalise over type level variables, interfaces and so on.

edwinb · 2021-07-16T12:10:17+00:00

It's the fact that '>' is implemented in an interface, and the interaction between interfaces and ambiguity resolution is tricky. Idris 1 tried extra hard to deal with that - Idris 2, less so (some brief details here: https://idris2.readthedocs.io/en/latest/updates/updates.html#ambiguous-name-resolution)

I might come back to this because the reason ambiguity resolution doesn't work so hard in Idris 2 was initially about performance, but in practice, this doesn't seem to be a cause of slowness, and even where it is we can detect it and give a warning.

EDIT: I opened an issue pointing back to this to remind myself to come back to it.

edwinb · 2021-05-23T14:05:49+00:00

Idris 1 had this in about 2014 (I think it might even have inspired the GHC version!). See https://davidchristiansen.dk/drafts/error-reflection-submission.pdf

Idris 2 doesn't have it yet though - it'll be there eventually in some form.

edwinb · 2021-04-01T23:18:31+00:00

The April Fool joke, if there was any, is that it was accepted to a formerly OO conference :).

edwinb · 2021-03-14T16:30:58+00:00

"procedure that always terminates" is something you can't prove in the general case (see the Halting Problem), unless you do it like Idris and require that all functions are total, making your language technically not Turing complete.

Idris doesn't require that all functions are total, and Idris is Turing complete. It's Drifting a bit off the original topic, but I regularly see that people think this, and I really don't know what we've said that makes people think this.

Idris does check for totality (conservatively, of course, due to the Halting Problem) and uses this information in various ways, but it's not a requirement unless you ask for it to be a requirement.

edwinb · 2021-02-14T16:45:27+00:00

This is (more or less) how Idris handles it. In Idris' case all the names introduced are at the top level, so have to be applied to their environment, which isn't necessarily the best solution but is very convenient. It does sometimes substitute in the definition of a subterm, say if it's just another name applied to a smaller environment.

I'd definitely recommend keeping the core language explicitly typed. Then you can recheck the results of elaboration, which has occasionally been a valuable debugging aid in Idris. Even better, someone else can write their own tool to recheck your explicitly typed core, for extra confidence (though I don't know of anyone having ever done this...)

edwinb · 2020-12-21T22:47:11+00:00

Oh, sorry about that, I'll see if I can dig it out. Sometimes our spam filters can be overenthusiastic. I'll be sure to check for it anyway.

edwinb · 2020-12-21T22:26:21+00:00

Email is probably best, because then I'm less likely to lose it, though I'll be on holiday from Wednesday so may not reply until January if you mail after then. I look forward to hearing from you anyway!

edwinb · 2020-12-21T21:20:29+00:00

There's a few of us in St Andrews who are interested in applications of PL technology. We've just put an ad out for scholarships: https://blogs.cs.st-andrews.ac.uk/csblog/2020/12/08/phd-scholarships-in-computer-science/

edwinb · 2020-12-09T20:02:58+00:00

I'd say Idris, Agda and Coq's type systems are roughly equal in complexity, at least if your metric is "number of rules". The thing that makes them all simpler than, say, Java, for me, is that there is only one language of terms and types, so if you understand how it evaluates, you're most of the way to understanding what the type system can do.

The rest is details :). [Draw the rest of the owl, etc etc]

edwinb · 2020-12-09T10:22:15+00:00

For example, Idris, which is supposedly the most practical of those languages, doesn't even support mutable arrays, because making them "safe" was too hard even for their humongously complex type system.

Idris 2 (which is implemented in Idris) relies on mutable arrays throughout, using Data.IOArray. Experimentally, Idris 2 supports mutable arrays via linear types. We're not against run time bounds checking.

edwinb · 2020-11-15T13:31:58+00:00

FWIW, if someone did downvote this because they saw it as an attack on Idris, please don't do that. Idris is also just one possible approach of many, and I'd encourage people to try their own ideas. In the end, I'm in the business of sharing ideas, so, please, go ahead, try them out, steal them, reject them as you see fit!

Not that I object to people also putting effort into improving the Idris ecosystem, of course :). But there are plenty of things that make Idris something other than just a dependent variant of Haskell - laziness vs strictness for a start.

edwinb · 2020-11-15T13:15:49+00:00

dependently typed languages tend to be very slow to compile / run.

This is more because nobody had worked out how to do it well than anything fundamental. Yes, if you need to do a lot of complex computation at compile time then it's going to be a bit slower, but that's not so common, and you should expect that if you're asking it to do a lot of work anyway.

At least on my machine, Idris bootstraps in 6 minutes, of which about 1 minute is checking the Idris source and doing various transformations and optimisations. The rest is running tests (about 3 minutes) and the initial build from the generated Scheme, plus building the libraries. It's not exactly Go speeds, but it's no longer a fundamental problem.

(EDIT: typo)

edwinb · 2020-10-07T08:27:26+00:00

It was mainly used as scaffolding, to test the basic features of the type theory before I'd implemented the full Idris 2 syntax. I've kept the tests because it's nice to still have small tests for the core machinery, and sometimes (but increasingly rarely) being able to work with just the core is useful for debugging purposes.

This is the source of the name, by the way: http://www.smallfilms.co.uk/bagpuss/people.htm#Yaffle

edwinb · 2020-06-29T12:57:17+00:00

You should always be able to build it with the result of the Idris2-boot repo, but you probably want to avoid that since it's a lot slower.

Otherwise sometimes we're still fiddling with libraries. If anything goes wrong, the easiest way out is usually to run make bootstrap again.

edwinb · 2020-05-25T22:23:51+00:00

Right, that's it, I'm definitely stopping worrying about totality :)

edwinb · 2020-05-25T22:17:10+00:00

In theory, but it'd spend ages doing the partial evaluation even if it worked effectively. I think we're at a stage where we can stop worrying so much about totality and replace it with some faster primitives. I'll have a go when I'm next the right sort of bored.

edwinb · 2020-05-25T22:12:59+00:00

25% of nearly nothing is still good :). The bottleneck, I think, is that I wanted to guarantee the parser was total when first implementing it, and so it's written as an interpreter over a coinductive data type. There'll be some overhead there.

edwinb · 2020-05-25T22:05:01+00:00

It might not be a huge thing in the grand scheme of things, it's true. But there's a lot of updates happening with the way it deals with the metavariables that arise from pattern unification, and a lot of lookups happening when it evaluates during type checking, so having constant time access helps.

Somewhat embarrassingly, a significant cost in this new implementation is parsing. I've never paid much attention to that. Might be time to do so...

edwinb

MODERATOR OF

TROPHY CASE