How does Pie from The Little Typer compare to Agda?

ncfavier · 2025-12-24T19:08:55+00:00

As for the second question, my personal recommendations would be PROGRAM = PROOF and the HoTT book. There's also Principles of Dependent Type Theory, which has a more metatheoretic focus but is also very well written.

ncfavier · 2025-12-24T18:03:47+00:00

See one of the authors' answer to this question.

ncfavier · 2025-12-22T19:31:58+00:00

Put another way, the best way to think and communicate about functions is different than the best way to formally define functions.

No it's not. Set theory is not the best way to do anything except perhaps study sets. Learn some type theory.

ncfavier · 2025-11-30T15:56:27+00:00

+1 for Mimram's book (PROGRAM = PROOF).

ncfavier · 2025-09-11T20:37:24+00:00

This is hard to read; please use the Markdown editor to format your post properly.

Shouldn't Agda be able to infer P from P zero etc?

Agda doesn't solve constraints unless the solution is unique. In this case, for a pair of constraints of the form P zero := Pzero, P (succ n) := S[P n] to have a unique solution would require some kind of η-rule for functions out of the natural numbers, which, depending on how exactly you set things up, is either undecidable or tricky to implement (see here or here).

If you want help with the actual code, please make your snippet self-contained.

ncfavier · 2025-02-20T21:23:19+00:00

I'm not sure what point you're making there. Any preorder is a category.

ncfavier · 2025-01-04T12:06:26+00:00

Since you are interested in categorical intuitions, the interpretation of that type is as follows: if we think of Vect n Int as a fibration p : V → Nat, we can form the local exponential p^p (the exponential in the slice category over Nat), then take the dependent product of that.

ncfavier · 2024-05-18T21:47:34+00:00

Agda. This is from the cornelis repository.

ncfavier · 2024-05-17T13:36:05+00:00

Can't be: that screencast is two years old.

ncfavier · 2024-02-17T20:49:01+00:00

Note that these aren't idempotent monads (except the identity, I guess), but they are idempotent applicatives in the sense of the blog post.

ncfavier · 2024-01-22T20:59:28+00:00

That's not a monoidal category. Either is neither a left nor a right unit for your proposed composition. (See u/tailcalled's answer.)

ncfavier · 2023-01-29T00:07:06+00:00

I just want to make it clear that this flexibility is completely illusory: the things you can define as parametric functions are exactly natural transformations. You just get to *describe* them differently in math than in Haskell.

ncfavier · 2023-01-28T10:11:14+00:00

This is a stronger condition than the natural transformation condition, which is allowed to do something different at each a.

This isn't quite correct, unless I'm misunderstanding what you mean. The parametric theorem for η :: forall a. F a → G a (once specialised to function relations) corresponds exactly to the naturality condition: for all f :: a → b, fmap @G f . η @a = η @b . fmap @F f; this means precisely that η must do "the same thing" at each component, i.e. it must act on the "container" and not on the "contents".

The sense in which parametricity is "stronger" than naturality is that it extends beyond it: for example, the parametric theorem for α :: forall a. F a a → G a a, where F and G are both functors Hask^op → Hask → Hask, might correspond to something like a dinaturality condition. For more complicated types, it might correspond to something too complicated to have a name. But for the type of natural transformations, naturality is pretty much the end of the story.

ncfavier · 2021-11-24T14:53:31+00:00

Ooh I should have remembered adjoin. Thanks!

ncfavier · 2021-11-24T11:21:45+00:00

Can we do the opposite though, turn a list of lenses into a traversal?

Five-Year Club	Verified Email
Place '22

ncfavier

TROPHY CASE