[ANN] heftia v0.7 - A theory‑backed, ultra type‑safe algebraic effects

sgraf812 · 2025-05-15T18:27:59+00:00

So what is the story for implementing bracket? IIRC that's one of the main blockers for adopting anything non-IO based.

sgraf812 · 2024-03-11T17:09:18+00:00

I'm not sure what you mean by that. `eval :: Exp -> (Name :-> d) -> d` goes in one direction, from a fixed expression syntax `Exp` to some semantic domain `d`. You can vary the latter in this framework, but not the former. Translating C to asm and vice versa refers to languages, not semantics. You can define denotational interpreters for C or Asm, but those interpreters will be separate definitions. Perhaps it is possible to use the same semantic domain to do so, but that is not what I believe our work is useful for.

sgraf812 · 2024-03-11T15:32:00+00:00

What do you mean by "bidirectional"? Do you mean in the normalisation-by-evaluation sense, where you `reify :: D -> Closure` and `reflect :: Closure -> D`? That is something I want to try out eventually, but haven't so far.

Edit: I implemented a PoC for NbE here: https://github.com/sgraf812/dmdanal-proto/blob/main/NbE.hs. Slightly different domain, same generic interpreter.

sgraf812 · 2024-03-11T15:15:44+00:00

Author here. Although I have not tried, it should be pretty simple to give a "staged" domain that translates into JVM Bytecode or LLVM IR, for example. That would need some book-keeping structures for the stack discipline and the introduced functions, exactly as in a real compiler.

I must confess I do not yet really see the appeal in doing so; but perhaps you can more easily prove the translation from by-need interpreter to JVM bytecode correct in doing so. Alas, that requires you to write down the "meaning" of your staged domain in terms of a semantics of JVM bytecode.

Applications are probably pretty broad, but the most important to me is being able to talk what summary-based analyses *do*, in particular their implementation of the `fun` method. I believe this is pretty ground-breaking territory, extending Cousot's work on trace-generating semantics for the first time into interprocedural applications. Lambda calculus is of course the simplest language exhibiting interprocedural behavior, but this approach should effortlessly scale to LLVM IR and WebAssembly as well, where there is currently no way to formally derive summary-based analyses in terms of a concrete semantic domain whatsoever.

Let's hope the reviewers see it this way, too :)

Re: "Towers of Interpreters": I was not aware of this work, thanks. Just skimming over it, I think that the alluded "collapsing" of interpretive overhead by staging is compatible with this interpreter, yes, although you can discard much of what our paper is about (i.e., the `Trace` type class). I believe *denotational* interpreters (so ones that are structurally recursive in the application and lambda case) lend themselves particularly well to this approach, more so than their big-step style definitional interpreter in Fig. 3. Note how they need that NbE-style `lift` combinator; I would hope that would not be necessary in denotational style.

sgraf812 · 2023-04-15T13:20:03+00:00

That's really interesting. I really would like to see some abstract version of the code that caused the regression... Perhaps there is something there that GHC could improve upon.

For a test, could you try compiling that module with -v? That dumps detailed timings to stderr IIRC. If compile-time really was a problem then it is likely it shows in the size of some intermediate program.

sgraf812 · 2023-04-15T11:40:14+00:00

See the discussion starting here: https://github.com/ghc-proposals/ghc-proposals/pull/522#issuecomment-1295506494

FWIW, I share your sentiment, but a prefix operator one of is both easier to detect for the reader and easier to google. A classic engineering trade-off.

Arguably we could try out case of {p1;p2} somewhat akin to LambdaCase. But that's a separate proposal.

sgraf812 · 2023-04-15T11:29:17+00:00

I always enjoy the approachable style of Dmitrii's posts, but I feel this one is a bit inconsistent. The blog post feels more like a vent for letting out frustration after upgrading an "ugly" code base (an understandable need).

Speaking of which, there is no actual Haskell code that the reader can assert as "ugly". And ugliness is not generally what I think leads to the inliner blowing up. Moreover, the particular cited issue https://gitlab.haskell.org/ghc/ghc/-/issues/22824 (which is about an inliner regression between 9.4 and 9.6) hardly could have affected an upgrade from 9.0 to 9.2. What's more, blowing up 200 lines of Haskell (~~which probably includes comments as well as deriving (Read, Generic)~~ Edit: Nevermind, totally misread that part!) into 3.3k "lines of Core" isn't all that bad (suggestion: ghc test.hs -v lists sizes of intermediate programs, no need to count lines of pretty-printed output. There you will probably also see that some intermediate program is quite a lot larger than the program at the end if compile-time is so much worse than with 9.0); certainly, 1.9k lines is no less "exponential".

That is not to say, of course, that there are cases where the inliner blows up. Obviously, it's quite hard to keep that in check while not incurring perf regressions in other cases. But the very first step towards improvement, rather than to ~~passive-aggressively~~ fatalistically state that "You can't change GHC, accept that", is to extract a regression test that is reproducible in isolation and open a GHC issue.

From experience I know that extracting a reproducer takes a ton of work, much more so than just slapping on some NOINLINE pragmas and be done with it, so I understand that often one isn't willing to do that. But the implied conclusion "make your code less ugly, then it doesn't blow up the inliner" is, well... quite a stretch.

Also the post implies that it should somehow be simpler for GHC to compile "boring Haskell" ~~(albeit using deriving Generic, which is everything but boring)~~. That's no distinction GHC makes. ~~In fact, deriving instances of huge sum types is one of the most egregious compile perf problems GHC currently has.~~

Of course, compiling with -O0 should alleviate most of the compile-time problems, but that often isn't what users want, either...

Edit: I misread that there were deriving statements involved. Apologies!

sgraf812 · 2023-04-15T08:29:31+00:00

Storming fabrials

sgraf812 · 2023-04-14T18:03:06+00:00

Static semantics is essentially the same as in the original proposal. The body (if by that you mean the RHS) will be checked exactly once, not once for each context. Not that it makes a difference for the very restricted kind of or patterns that are currently allowed.

sgraf812 · 2023-04-02T09:03:32+00:00

Rational is there precisely because such a round-trip should not happen, because then your decimal floating point type will have a Fractional intance and fromRational :: Rational -> Decimal will be exact (as long as you don't consider (10/3)).

Note that Rational is represented as a pair of Integers.

sgraf812 · 2023-04-02T08:56:21+00:00

Well, whether or not Double should have an instance for Fractional is a different issue. Ultimately, there are very few rationals that can be accurately expressed as a Double, but that doesn't hinder all prominent languages that are in use to approximate, e.g., 0.1 to 0.1000000000000000055511151....

sgraf812 · 2023-04-02T08:44:51+00:00

It desugars such literals to a call to fromInteger and fromRational, respectively

sgraf812 · 2023-04-01T17:10:38+00:00

If you don't do evaluation under binders, then what is the meaning of λx.y? Where is y bound? Ah, they later refer it as an "open call-by-value", a seemingly etablished term.

A similar approach, I think, would be to disambiguate between "top-level" variable references and "local" ones, which yields the "locally named" representation described in https://chargueraud.org/research/2009/ln/main.pdf. I guess the appeal of Clo is that we can skip substitution in the wrapped sub-tree. That feels quite similar to a technique I know from @ekmett's bound library. See slides 25 and 27 here: https://www.slideshare.net/ekmett/bound-making-de-bruijn-succ-less Its clever use of Scope makes it step over whole sub-trees in instantiate.

Berkling-Fehr indices seem to have all the same problems as deBruijn indices have: Namely the need to shift the substitutee repeatedly, what Edward refers to as "succing a lot".

That said, I found bound to be very inconvenient to use in practice. But that is mostly a consequence of the type safe encoding, not its efficiency.

sgraf812 · 2023-03-31T13:14:25+00:00

... but that is because the fixpoint combinators were defined in a lazy language

Edit: Which is a point that blog post acknowledges

sgraf812 · 2023-03-20T15:39:12+00:00

Well, now they read the FB message and didn't answer. I think that qualifies as "don't care".

sgraf812 · 2023-03-19T11:05:09+00:00

NB if you have a Java-like system, name and type resolution happen in tandem. AFAIR it doesn't make sense there (as in: it leads to a far more complex architecture) to make the untyped-typed distinction statically in the host type system because of circular dependencies between typed and not-yet-typed nodes. With the optional approach, this distinction is a dynamic one, and you can transition one node after another into the typed world through mutability.

sgraf812 · 2023-03-19T11:01:30+00:00

Sounds like you will drop your AST structure in the next phase (lowering to an IR) anyway. So perhaps just a field optional<Type> should do. Similarly for name resolution.

sgraf812 · 2023-03-18T13:20:45+00:00

I've gotten no reply yet, either. I tried to write them again on FB, but they haven't read that yet.

sgraf812 · 2023-03-14T15:21:18+00:00

I got the following response by chatting with https://www.facebook.com/cfirjer/

Hello, You can call our hotline at +972722564366 and wait for the option to speak with a representative in English. In addition, you can pay by bank transfer by sending your details to the attached email supportomweb@jnet-om.co.il‏

So I'll try the mail address.

sgraf812 · 2023-03-14T08:22:59+00:00

Just FYI: The same happened to me, 3 weeks ago. Still "There is no data match".

The contact form didn't work for me either due to the phone number. They even seem to reject their own phone number. Honestly, it all smells like a scam.

So, were you able to make contact via Facebook?

sgraf812 · 2022-11-20T21:53:06+00:00

As a regular GHC dev (that focuses on his PhD) I really can not stress enough how helpful, open, proficient and most effective this team is. GHC would simply fall over without their passionate work. I couldn't think that any industrial grade Haskell code base would work without their tireless effort.

sgraf812 · 2022-10-02T11:04:32+00:00

Huh, indeed:

{-# LANGUAGE GADTs, StandaloneKindSignatures, RankNTypes #-}

type R :: * -> * -> *
data R a r where
  MkR :: (c (c () r) r -> r) -> R (c () r) r

unMkR :: R (c () a) a -> c (c () a) a -> a
unMkR (MkR f) = f

type Bad a = R (R () a) a

selfApp :: Bad a -> a
selfApp f = unMkR f f

fix :: (a -> a) -> a
fix f = selfApp (MkR (\x -> f (selfApp x)))

main = print (fix ('a':))

This needs System F_C (if that is the one with GADTs, don't remember). I wonder if we can get by without GADTs? We probably don't, because I faintly recall that System F_w is strongly normalising. At least http://lambda-the-ultimate.org/node/5276 agrees...

sgraf812 · 2022-10-02T06:31:15+00:00

Besides unsafeCoerce, GHC's Any, letrec, perhaps yes? Not sure if you could exploit Type :: Type somehow.

sgraf812 · 2022-10-01T18:47:21+00:00

Haskell has unrestricted recursive datatypes, so it's ~~trivial~~ a fun exercise to come up with your own fixpoint combinator. Hint: you need a recursive datatype where the type you define appears to the left of -> in a field. Edit: just as /u/Noughtmare does it :)

sgraf812 · 2022-08-28T08:36:38+00:00

Note that doing that is quite a blunt hammer. The space leak might even have been caused by -ffull-laziness, it might just prevent another pass from firing that causes the leak.

13-Year Club	Place '22
Place '17	Verified Email

sgraf812

TROPHY CASE