Edward Kmett

`a -> m ()` for m a Monad is effectively `a -> Ap m ()` which is `Op (Ap m ()) a` should have effectively all the instances you'd expect for this.

Notice that Comonad and Contravariant have nothing to do with one another. A Comonad is still a _covariant_ Functor.

pure'ish :: Applicative m => ( () -> a) -> m a
conquer'ish :: Divisible m => (a -> ()) -> m a

empty'ish :: Alternative m => (Void -> a) -> m a
lose'ish :: Decidable m => (a -> Void) -> m a

These rewrite into the forms of pure/conquer/empty/lose by using uniqueness of initial/terminal morphisms.

Edward Kmett on X: "GPUs made training massive models possible, but inference needs better memory capacity, memory bandwidth utilization, more power efficiency, and an architecture built bottom up with transformers in mind. To that end, I'm excited to share that Positron just raised a $51.6M Series https://t.co/5NjFMjZ9FP" / X GPUs made training massive models possible, but inference needs better memory capacity, memory bandwidth utilization, more power efficiency, and an architecture built bottom up with transformers in mind. To that end, I'm excited to share that Positron just raised a $51.6M Series https://t.co/5NjFMjZ9FP

To celebrate that writeup, the folks in the lab put together a schlocky little promo spot, which I couldn't resist sharing here. [No production cards were harmed during the filming of this video.]

Apologies for the twitter link, but it was over the local 3 minute limit.

x.com/kmett/status...

The New Chips Designed to Solve AI’s Energy Problem Tech giants and startups alike are trying new approaches to what has been a vexing problem.

www.wsj.com/tech/ai/the-...

I'm proud of what the Positron AI team has accomplished and I'm grateful to our investors Valor Equity Partners, Atreides Management, and DFJ Growth for backing us!

We offer solutions that are already deployed and are shipping today, and we've designed new silicon to reshape AI inference—reducing cost, drastically cutting power consumption, and unlocking entirely new capabilities in production AI environments.

GPUs made training massive models possible, but inference needs better memory capacity, memory bandwidth utilization, more power efficiency, and an architecture built bottom up with transformers in mind.

To that end, I'm excited to share that Positron AI just raised a $51.6M Series A!

Not sure any of that was useful but that was pretty much everything I had that came to mind offhand.

Another more traditional tool for this sort of thing where information flows both ways is to use an attribute grammar and synthesize to pull information up and inherit to push information down through a syntax tree.

When constructing ZK proofs for a lazy language, I also wind up in something like this situation, where I might squirrel away info about what thunks are going to be used in a pre-run, so I can rearrange calculations to the let binding site of the thunks I actually need, rather than the case site.

Another way to think of this is in terms of modalities. The Tardis gives you access to both forward and backwards facing information about contraction and weakening, but its use here ties this to situations where you've committed hard to your inputs, not like a traditional typechecker time pass.

mail.haskell.org/pipermail/ha... was me doing something kind of similar using Codensity STM rather than Tardis to look forward into the future to determine if a reference was used.

One-bit-reference counts can be refreshed by a custom GC, and ensure a tight analysis, and I've used it to patch up a shoddy type-checking-time uniqueness check. OTOH you seem to be doing this after being given user values, so you kind of muddy the waters from how I usually see it done.

I don't really like the precision I usually see with uniqueness analysis-done-at-compile type for instance, and that looks _kind_ of like what you are doing. (caveats later)

I have a scattershot of thoughts, and it's hard to fit them into a single message here, so I apologize if I wander. Still trying to learn how to use the multi-comment editing features on bluesky, so I might make a right hash of THAT as well. Here goes:

You are looking at a particular bit of information (its generating function) which you can extract from an arbitrary Joyal-style combinatorial species. Most models of ADTs limit themselves to a nicely closed subset of species that generate merely ordinary generating functions, though.

You're basically describing (finite) data structures in terms of their associated ordinary generating functions.

comonad.com/reader/2008/...

You can define sums, products, etc. this way.

If you go to exponential generating functions, you can also include bags, and cycles.

They clearly named this animal house for John Belusk^Hhi.

We retired the evil mangler, so at least that perl isn't touching every chunk of assembly produced by the compiler any more!

*@kmett.ai now

@bartoszmilewski.bsky.social just joined.

Hi Bartosz!

There'a a lot of neat tricks buried in there.

I generally agree on the mutable variable advice. That said, Adam Gundry's PhD dissertation really showed what is possible with the alternative:

adam.gundry.co.uk/pub/thesis/

In particular he makes good use of explicit contexts to carefully track issues that arise as types get more dependent.

It acted as a forcing function for me to register the domain, \@comonad.com and \@kmettgroup.com seemed like odd choices of handles, and my other domains are just weird. Too bad I let kmett.com go by accident a decade or two ago.

a man in a suit is standing in a dark room and saying captain ! my captain ! ALT: a man in a suit is standing in a dark room and saying captain ! my captain !

They wouldn't call it a standing desk if you weren't supposed to stand on it.

In theory we _should_ be able to come up with some kind of low cost dwarf-compatible way to dump this info. It is accessed rarely. The demand-based stack is there, even though the stack isn't a "c stack". It's just the logical "syntactic" call stack that needs maintenance via something lighter.

I don't know how to do this with low performance cost. Do you?

When you turn on enough profiling you get some support out of HasCallStack regardless, but tracing that changes runtime behavior non-trivially and incurs costs.

I complain about this too, but don't have a viable alternative to offer.

The main issue with 'usable stack traces' in Haskell, is there are two notions of that.

One is the trace of what you are forcing that led to this point.

One is the trace of syntactically what led you to this point.

They are very different. That said, you can basically get both with HasCallStack.

can confirm