Epic & Monic is not Iso!

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 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 ...

I am looking for a SWE position remote if possible. If you like what I write about and want to see a CV send an email!

An apologia of lazy evaluation As a programming language, laziness is the definitive feature of Haskell. Every other quality such as: higher order functions, Hindler-Milner type system or being lambda calculus based is present on other languages. In fact Haskell was born as a committee initiated language to avoid a proliferation of non-strict languages at the end of the 80's, putting all the effort before the same cart. If you take some time, and look at what HN , stack overflow or reddit has to say about the general sentiment of non Haskell programmer on laziness, it could be resumed on a single word: anxiety . It seems that space leaks due to laziness are unavoidable and that Haskell programmers choose to live with them. The methods of detecting them come from dynamic analysis of compiled programs . There is no general advice on how to avoid them apart from experience; an even then it not enough, as expert Haskell programmers still trip over them time to time. What hope do ...