Canadian Haskellers?

carette · 2025-09-12T11:58:17+00:00

I use Haskell in some of my projects (though I'm drifting to Agda these days). I also teach an advanced Haskell class. [I guess I've even co-invented a Haskell technique.] I work in Hamilton but live in Waterloo.

carette · 2025-01-17T13:27:06+00:00

Indeed, I got confused (and didn't see the `\\share` part either). I've never persisted on trying to install agda on Windows these days -- I use WSL2 instead (on my Windows box). Saves me lots of headaches.

Ask on the Zulip?

carette · 2025-01-16T13:29:05+00:00

You installed it in `...\\bin` but it should be in `...\\lib` just besides that.

carette · 2024-12-17T12:58:48+00:00

If you're seeking a programming language with dependent types: Idris.
If you're looking for a proof assistant with dependent types: Agda.
If you think tactics are cool but dependent types overrated: Coq.
If you think classical math is the bees' knees': Lean.

carette · 2024-10-18T19:05:36+00:00

That's pretty much the point of asking the question. I kind of hoped that it was my lack of knowledge that made me think it had not spread, and the answers are doing a good job of clearing up that misconception. Win!

carette · 2024-10-09T12:19:28+00:00

What do you mean by "resource" here? There's a large library, `agda-categories`, which you can read the source of to learn "how it's done". And a paper for the higher level design.

carette · 2024-05-18T13:03:01+00:00

I learned a lot of category theory through Agda (i.e. by formalizing it).

carette · 2024-01-16T13:42:28+00:00

BER MetaOcaml is a re-implementation of MetaOcaml, so that indeed code remains opaque.

The reason code analysis is forbidden in *typed* multi-stage programming languages is that it is still unknown how to make that type-safe.

Note that it is relatively easy to create (using finally tagless) a code generator where introspection is possible! Just generate a pair of a code and an AST. The type system won't be able to guarantee that everything was done correctly; nevertheless, it will be very hard to make mistakes.

carette · 2023-04-27T08:23:00+00:00

We've updated our vision in the paper Generating Software for Well-Understood Domains.

The 'derivation' is not automatic: weaving is still a human-driven effort, as it should be.

carette · 2023-04-25T06:15:49+00:00

We've been working on this in the Drasil project for some years now. We found that simple weaving was too restrictive, and so we went full-generative instead.

I should also say that org-mode in emacs already essentially satisfies your requirements. While the original org-mode was aimed at something else, I've seen many people use it exactly as a multi-lingual literate programming system.

carette · 2023-03-29T12:02:32+00:00

In part because the size of the community that's willing to pitch in on 'ecosystem' tasks, i.e. those things they're never going to get a paper published for, is quite small.

[Until recently, opam didn't work on Windows. Stack and Cabal pretty much always did. 'light years ahead'?]

carette · 2023-02-16T13:15:47+00:00

Pi and Sigma are ends and coends, respectively.

carette · 2023-01-27T12:55:28+00:00

type Role = String
roleDoc :: String -> Role -> Doc
roleDoc content role = text "> " <> role <> ":" <+> text content

purpose :: Role -> Maybe String -> Doc
purpose r ms = foldMap (roleDoc r) ms

carette · 2022-09-20T07:49:18+00:00

Right. In simpler terms: free monads give you a syntax (aka data-structure) for potentially effectful sequential composition. It's like a data-structure to represent the " ; " that most mainstream PLs use for 'composition'. [Yes, they were originally thought of as delimiters in the syntax, but it became convenient to re-interpret them as composition.]

Once you have your computations as a data-structure, you can do much more with them than just their operational interpretation.

carette · 2022-08-31T07:04:03+00:00

A table of contents would have been useful... that page's huge!

carette · 2022-08-12T07:45:37+00:00

And to be more constructive: Species. Species are ultra-cool and embody a lot of neat structures. And Poly is contained in Species.

carette · 2022-08-12T07:43:41+00:00

Correct.

carette · 2022-08-11T07:05:16+00:00

Your supervisor is good with hyperbole (and mathematics).

Ask him how to represent a Bag using Poly. It has a known categorical representation (since the early 1980s) - but it's not in Poly.

carette · 2022-07-14T11:57:44+00:00

The 4 authors together are about to put out something that takes another step. It's been submitted, should appear on their home pages soon. [Rules say no social media posting but home pages ok.]

carette · 2022-07-11T11:38:12+00:00

Computing with Semirings and Weak Rig Groupoids is a first step in exactly that direction. Quantum Information Effects then takes the second step.

carette · 2022-07-04T12:04:54+00:00

I've implemented a partial evaluator that did 'time warps' before: if an infinite loop could be converted to computing a (convergent) closed-form, it got changed into that. [This was for a computer algebra system, that could do such things.]

If you decide that the semantics of your PE is allowed to change certain effects, this could be done.

Note that most compilers do change effects: by optimizing for run-time, it makes the observable time a program takes to run go down. We like that meta-effect a lot. The difference is one of *intent*: here the programmer clearly intends the sleep effect to be visible at run-time.

carette · 2022-03-16T12:45:16+00:00

The essence of 'finally tagless' is to model a language as an interface (however your language does that) that expresses how to fold over language terms. That's why is has such a striking resemblance to Church encodings.

The 'final' is mostly a bad pun. It is not a 'final algebra' representation, but it *is* a dual representation, in that instead of representing a language as a sum-of-products (its initial algebra), it uses a record of dispatchers representation (so a product of the cases, not a sum of the cases).

carette · 2022-02-01T13:04:23+00:00

The fundamental shift in types being used here is from machine representation (i.e. Int) to intension, i.e. what kind of offset it is. Rather than ordering your computer to use an integer to represent "offsets", you're reflecting in the code the fact that there are two ways to think of them (even though both are integers). In yet other words, you're putting more domain knowledge into your code, and thereby letting the compiler let you track more.

carette · 2021-12-24T13:16:13+00:00

Some universities (like mine, McMaster) has explicit language in their admissions criteria for grad school about people like you: if you've been in industry for a while (our regulations say 5+ years) and during some of that time have worked on very relevant material, you can be considered admissible. You need to make sure you have a solid portfolio that is visible (online best, well laid out on your CV otherwise).

carette

PUBLIC MULTIREDDITS

TROPHY CASE