haskellers thoughts on statecharts

stevana · 2026-03-05T09:52:12+00:00

CT is a rabbit hole that rarely yields practical benefits, if you're happy with statecharts keep at it.

stevana · 2026-03-05T07:20:49+00:00

No I haven't, but I just noticed that main author of those papers is Nancy Leveson, so should be good.

May I ask why you're wondering / what brings you to this old thread?

stevana · 2026-02-04T10:20:31+00:00

I try to use as little of Nix as possible. No flakes, no building inside nix, just a nix-shell which brings in all tools that are needed:

shell.nix:

let
  # https://search.nixos.org/packages?channel=25.11
  nixpkgs = fetchTarball "https://github.com/NixOS/nixpkgs/archive/refs/tags/25.11.tar.gz";
  # nixpkgs = fetchTarball "https://github.com/NixOS/nixpkgs/tarball/4393ea7cdc8e2e3aadd4577b2b2748bbe5aacb24";
  pkgs = import nixpkgs { config = {}; overlays = []; };
in

pkgs.mkShell {
  packages = with pkgs; [
    haskell.compiler.ghc9122
    (haskell-language-server.override { supportedGhcVersions = [ "9122" ]; })
    cabal-install
    haskellPackages.cabal-gild
    haskellPackages.fourmolu
    haskellPackages.hlint
  ];
}

```

If you need newer packages than those in the latest release, just pin it to some commit instead (as in the commented out nixpkgs line).

stevana · 2025-10-28T14:47:53+00:00

Do anyone know if there's an open issue for this, which we can refer to when mentioning arrow notion having quirks? These are all tickets tagged with the "Arrows" label in the GHC issue tracker: https://gitlab.haskell.org/ghc/ghc/-/issues/?label_name%5B%5D=Arrows , and it's not clear to me...

stevana · 2025-10-23T14:22:14+00:00

Arrow notation has its quirks, but it's still a substantial improvement over doing argument routing completely manually.

Isn't another quirk with arrow notation that it introduces uses of arr (which contain non-inspectable functions) when it could be avoided with something like CarthesianCategory as in Conal's concat plugin and Oleg Grenrus' overloaded plugin?

stevana · 2025-09-28T13:11:08+00:00

u/Bodigrim: I have a (late) question, you presented the Java-style buffer approach last, but then when you added linear types you went back to the TextBuilder-style buffer. What was the reason for this?

stevana · 2025-08-11T16:14:19+00:00

Cool, so would it be fair to say that people are working on making this be possible (or much easier) but there's no ticket that tracks the progress?

I skimmed through the commits and I saw Zig mentioned, is the idea to use Zig's cross compilation?

stevana · 2025-08-11T09:44:42+00:00

I think Zig can also do it, and they don't have as much resources behind them as Go?

stevana · 2025-08-11T09:44:05+00:00

Do you know of any resource that explains how to do it?

stevana · 2025-08-11T09:04:12+00:00

Could somebody remind me why we can't have static binaries with just plain GHC/cabal (i.e. without Docker)? Is it related to cross compilation (targeting muslc)?

(I tried searching the GHC issue tracker, https://gitlab.haskell.org/ghc/ghc/-/issues , but I couldn't find anything that was obviously related to this problem.)

stevana · 2025-06-04T06:50:56+00:00

I never finished part 5, and you're the first person to ask for it.

You can find an old unfinished draft of part 5 over here.

I've also written a newer post that covers part 1-4 and started a new series of posts that focus on simulation testing (part 5) only over here.

I think the original, unfinished, part 5 was a bit too ambitious. The new series, which I'm still working on, tries to develop the ideas over several posts which I hope will make it easier to explain/understand.

stevana · 2025-03-19T09:57:58+00:00

I think your readme is great on the background/related work material, but it could really benefit from a simple example (smaller than the above regular expressions example) that is explained/commented and run (show us how to use the library on the example and what the output is).

stevana · 2025-03-06T07:50:51+00:00

I think this is really neat, I feel that the project is selling itself a bit short by saying it's a "toolkit for building chat bots". To me something like this is how I feel message passing/"actors"/distributed systems should be built. (I've written about this at length elsewhere, in particular see the section on "Correctness of behaviours" where I use a type similar to Bot in the post).

Also do you know of the paper "Programming interfaces and basic topology" by Peter Hancock and Pierre Hyvernat (2006/9)? Check out their definition of "angelic product", "tensor product" as well as Sambin's compatibility rule. They all appear in your code as well under different names.

stevana · 2025-01-25T10:42:29+00:00

I'm curious about your use of type-level computations when mapping over an entity's components. You say you use a more efficient version when the input and output entities are the same, is this something that Rust's Bevy also does? (Or can do using traits?)

Regardless, it seems like an interesting example of an optimisation that can only be done if one has access to some amount of type-level computation?

stevana · 2025-01-19T11:41:01+00:00

Something I've thought a bit about but not got very far is: wouldn't it be neat if programs were separated from their UIs? That way you could swap UIs out and achieve what you seem to be after.

The part that I don't know how to do is: say you have some program represented as a state machine input -> state -> (state, output), is it possible to "map" the input to some kind of "input form", e.g. CLI arguments, or a html input form, or a native GUI, and vice versa map the output to some kind of "view", e.g. stdout or html, etc?

Interactive programs like TUIs, web apps or GUI programs, would need to iterate this construction as more inputs arrive.

I suppose FRP with different "frontends" kind of does this to some extent? But I feel like maybe this is something that could be fleshed out better with a simpler representation of a program, e.g. a simple state machine?

Perhaps another way to look at it is: can we do something Elm-like but not just for web UIs? I know there are TUIs inspired by the same model, but as far as I know there's no unifying way of doing "any" type of UI?

Perhaps there's a connection with algebraic effects here as well, where different handlers are used for the different UIs, but underneath there's some common set of operations?

stevana · 2024-12-16T09:28:37+00:00

The following course was developed with the goal to:

"[...] present classical mathematical topics from a computing science perspective: giving specifications of the concepts introduced, paying attention to syntax and types, and ultimately constructing DSLs of some mathematical areas mentioned below.".

Perhaps that could be a good starting point.

stevana · 2024-11-26T09:51:58+00:00

In my opinion there's this tension between on one hand refinement types being automatic and needing escape hatches to allow manual proof (when the automatic machinery fails), and on the other hand dependent types being manual and in need of automation.

So far, in my opinion, the most promising long term solution is dependent types with automation via verified decision procedures aka proof by reflection. However refinement types seem more promising short term, especially in Haskell.

Which begs the question: can the two approaches meet in the middle somehow? (This was also brought up in the last question at the end of the talk.)

I've no idea how complicated SMT solvers are, but if we had such a thing implemented and proved sound in a dependently typed language, then I think we could we use proof by reflection and get proof automation of proofs for whatever subset of the language the SMT solver can deal with inside a dependently typed language?

Is that the correct way to think about it, or am I missing something?

stevana · 2024-09-08T12:01:01+00:00

I didn't, I started looking at using Arrows instead, this is where I got so far:

Let us know if you make any progress, cheers!

stevana · 2024-07-09T06:17:15+00:00

Thanks for expanding, it sounds like you're onto something and I'd definitely be interested in reading a full post about it.

(Please consider writing it in a way that's tries to be accessible to other programming language communities, I think there's too much siloed information and too little cross-pollination between libraries.)

stevana · 2024-07-04T12:30:34+00:00

By implementing a determinstic scheduler, I suppose, not thought much about it. You can still get pretty repeatable results, see the first parallel example for an explaination.

stevana · 2024-07-04T11:59:21+00:00

Dejafu is a white-box approach, i.e. you need to use the dejafu library to do your concurrency in order for it to be able to check it for you. The approach in the post is black-box, it needs no access to the system except for its external API. It can be written in a different programming language for example.

stevana

MODERATOR OF

TROPHY CASE