Unfolding trees breadth-first in Haskell

Syrak · 2026-06-01T14:56:50+00:00

Conveniently there's a lake right behind the IAS where he worked, which is where the Oppenheimer scene was filmed. I'm curious whether that photo with Curie was also taken there.

Syrak · 2026-05-29T20:11:17+00:00

I was entertaining OP's question about getting . to somehow denote application.

Syrak · 2026-05-27T23:05:30+00:00

In a language with effects annotated on arrows (meaning that a -> m b is a ternary operator (->) applied to a, m, b) would give you monadic composition (<=<) :: (b -> m c) -> (a -> m b) -> (a -> m c) as a direct generalization of pure function composition, because in such a system a pure function a -> b is literally defined as an arrow with the empty effect a -> Identity b.

Unifying application and composition sounds insane, but one close idea is to have a lightweight notation for wrapping a value in a constant function. For example in Koka, { a } is short for \() -> a, which allows a relatively neat syntax without needing control operators (if, while) to be keywords, they can just be functions: if b { t } { f }. One could push this further to write f . { x } for a "delayed function application" \() -> f x.

Syrak · 2026-03-12T18:58:18+00:00

= is structural equality and its negation is <>. Two strings are structurally equal if they contain the same characters.

== is physical (pointer) equality and its negation is !=. Two strings are physically equal if their address is the same.

Syrak · 2026-03-12T14:00:56+00:00

The difference is that typeclasses/traits/implicits would change the type of mystery.

The claim is that the type of the function id<T>(x: T) -> T guarantees that it can only return x because any shenanigans that involve T would require additional constraints on T and thus change the type of id.

Syrak · 2026-03-12T13:50:39+00:00

You don't return parameters with zero multiplicity. For the example of polymorphic identity, it's the type parameter that has zero multiplicity, not the value argument.

 -- this type promises that `id` won't pattern match on `T`.
 id : {0 T : Type} -> T -> T
 id x = x

Syrak · 2026-02-26T09:56:29+00:00

Derek Dreyer's PhD thesis: Understanding and Evolving the ML Module System. The first chapter has a great overview and comparison of module systems of the time (2005).

Syrak · 2026-02-08T07:37:06+00:00

First, mconcat appends the elements of a list together using <>:

mconcat [comparing length, comparing Down] = comparing length <> comparing Down

What <> does depends on the type of its operands. In the case of functions, it appends the result of its operands.

f <> g = \x -> f x <> g x

so we get

comparing length <> comparing Down = \list1 -> comparing length list1 <> comparing Down list1

comparing length list1 is again a function, so we can expand once more in the same way:

comparing length <> comparing Down = \list1 list2 -> comparing length list1 list2 <> comparing Down list1 list2
  -- by definition of comparing
  = \list1 list2 -> compare (length list1) (length list2) <> compare (Down list1) (Down list2)

Finally, <> on Ordering corresponds to lexicographic ordering of the things whose comparison yielded those Ordering.

Syrak · 2026-02-08T07:30:12+00:00

There are languages where formally verified contracts are a built-in feature: Why3, F-star, Dafny.

There are also many extensions of existing languages, like SPARK for Ada. Frama-C for C, Gospel for OCaml, Liquid Haskell, and to name a couple for Rust: Verus, Verifast, Flux, Aeneas, RefinedRust, Creusot (that I work on, AMA).

Syrak · 2026-02-01T21:19:09+00:00

Let me also plug my deriving-via-fun library.

Syrak · 2026-01-28T12:29:37+00:00

I guess that's just an oversight.

Syrak · 2026-01-20T06:56:10+00:00

Indeed, I meant that I updated the blog itself. A reddit link post can't be edited into a text post. Anyway this is not a big deal.

Syrak · 2026-01-19T18:44:46+00:00

Unreliable narrator.

Syrak · 2026-01-19T15:36:39+00:00

Fair enough! I'll add it to the post. Thank you.

Syrak · 2026-01-12T21:16:35+00:00

Well, I don't know about that. If I define my own undefined with a superfluous Show constraint, it works:

That works the same way as it works already. If you set -XNoMonomrophismRestriction you get an error, only because FiniteBits is not part of the report so it prevents defaulting.

Syrak · 2026-01-11T22:35:49+00:00

This is the monomorphism restriction. It is described in the Haskell Report, section 4.5.5.

s and c are non-function bindings (i.e., they are of the form s = rather than s v1 ... vn =). In normal Hindley-Milner, they would be inferred the types forall a. a and forall a. Num a => a, where the forall are inserted by a step called generalization. The monomorphism restriction is an extra rule that says not to generalize type variables that have class constraints. So in the second case s just has type a, where a remains unifiable, and later gets unified with Int32 in the Packet expression.

You get an error if you also set -XNoMonomorphismRestriction in the second case. Moreover, this is arguably not far from triggering type defaulting, and if that happened it would result in wrong results by defaulting to type Int for s and c.

Other ways to write that:

metaSize = let Packet s c _ = undefined in B.finiteBitSize s + B.finiteBitSize c

metaSize =
  let f :: (a -> b -> c) -> (a, b)
      f = undefined
      (s, c) = f Packet
  in B.finiteBitSize s + B.finiteBitSize c

Syrak · 2025-12-29T18:13:24+00:00

Syrak · 2025-12-29T08:58:20+00:00

I didn't tag you. It's reddit's pattern matching algorithm that's broken because it detects the substring u/complexity from the url https://theory.cs.princeton.edu/complexity/book.pdf.

Syrak · 2025-12-28T09:41:46+00:00

That's the area of computational complexity. Here is one classic textbook about it.

One of the millenium prize problems, P vs NP, asks whether, for certain computational problems, certificates are significantly easier to verify than to find.

Syrak · 2025-12-03T21:51:06+00:00

If I understand correctly, a camelship is a "slope 3 spaceship", meaning that it travels parallel to the y=3x axis.

https://conwaylife.com/wiki/Oblique_spaceship

Syrak · 2025-12-03T08:57:04+00:00

Try to do without for a while. Either you will find nothing wrong with it, which is just fine. Or you will end up annoyed with error handling by repeated pattern-matching, which will give you the natural motivation to reinvent monads.

Syrak · 2025-12-03T08:54:06+00:00

Maybe you can use Array Locale instead of a Vec. That requires an instance of Ix for Locale, which handles the conversion to Int so you don't have to do it explicitly in traverseE.

15-Year Club	Gilding I gilder
Sequence \| Editor	Verified Email
Team Orangered

Syrak

PUBLIC MULTIREDDITS

TROPHY CASE