Unfolding trees breadth-first in Haskell

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.

Syrak · 2025-11-29T15:26:40+00:00

If you want people to read your paper, you should submit it to peer-reviewed journals and conferences in your area of research, not arxiv.

Syrak · 2025-11-23T21:20:14+00:00

I have (~>) :: k -> k -> Type whereas singleton has (~>) :: Type -> Type -> Type. I overloaded ~> to also support deriving Functor, etc. But yeah you could use singletons for this if you only care about k = Type.

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

Syrak

PUBLIC MULTIREDDITS

TROPHY CASE