Entradas

Mostrando las entradas de abril, 2023

Presenting data-forced, an alternative to bang patterns for long lived data structures

Presenting data-forced, an alternative to bang patterns for long lived data structures Table of Contents 1. The problem 2. The data-forced approach 3. UnliftedDatatypes have a different calling convention (CBV) 4. Conclusion As a consequence of my previous post , I crafted a new way to deal with liveness leaks : data-forced . It relies on CBV functions and tagging values when we know they have been evaluated. It is not complete, it is possible to be mis-used and not get any benefits, but it shows promise and gives stronger guarantees than the current status quo. Also, I am starting a new job next week, so I will have less time for hacking and writing. 1. The problem Long lived data structures that store thunks will keep the references needed to evaluate those thunks alive for a long time. This is a consequence of not pairing the denotation of the values with a good consumer. Current ways to deal with this on Haskell are: Use Bang patterns and/or se

A proof of \(\mathcal K \otimes V \cong V\) using the universal property of the tensor product (Category theory in context Edition 1, 2.3.ii.i)

A proof of \(\mathcal K \otimes V \cong V\) using the universal property of the tensor product (Category theory in context Edition 1, 2.3.ii.i) A proof of \(\mathcal K \otimes V \cong V\) using the universal property of the tensor product (Category theory in context Edition 1, 2.3.ii.i) Table of Contents 1. Uncle Yoneda will give you the basic framework 2. You should look at the functor \( \text{Vect}(\mathcal K \otimes W, -) \) 3. That \(\text{Vect}(k , -)\) is interesting tho 3.1. Lemma: for all \(Y\) vector spaces, \( \text{Vect}(k, Y) \cong Y \) as a vector space. 4. How does this help us? 5. OK cool, but that does not establish the result! 6. In the end I found this little exercise super fun, but it took me some days to finally see it. The question is this Let \(V\) be a vector space over a field \(\mathcal K\). Prove that \(V \cong \mathcal K \otimes V\). I will take a non-dry formal approach on how to see this is true. We will do this

How to avoid correctness space leaks on a lazy setting in haskell

How to avoid space leaks on lazy setting How to avoid space leaks on lazy setting Table of Contents 1. A classification of space leaks 2. Avoiding strictness leaks 2.1. Repeatedly used functions over the same expressions 2.2. Using cost centres and one weird trick to catch them at run-time 3. Avoiding Liveness leaks 4. Avoiding excessive sharing leaks 4.1. Merge multiple passes over the data structure on a single pass 4.2. Move the creation of the generator inside the function and wrap it on a dumb function 4.3. Bite the bullet and use linear types 5. Conclusion Some posters on HN on made the observation that on my previous post I did not give general advice on how to avoid space leaks. This is specially important given that I ceded the point that exists a cluster (b) of space leaks that are of a correctness concern. The tools at our disposal come in two varieties: Defensive coding patterns Running program profiling I think the first