"Type Theory and Functional Programming" by Simon Thompson (PDF available via quick search)

First 120 pages of "Type Theory and Formal Proof" by Rob Nederpelt / Herman Geuvers

For some early stuff on dependent types (also covered in the above), check out "Intuitionistic Type Theory" by Per Martin-Lof

"Computation and Reasoning: A Type Theory for Computer Science" by Zhaouhui Luo

"Type-Driven Development with Idris" by Edwin Brady

"Gentle Introduction to Dependent Types with Idris" by Boro Sitnikovski

"Types and Programming Languages" by Pierce

"Practical Foundations for Programming Languages" by Robert Harper (or any of his YouTube videos re/Type Theory)

"The Little Typer" by Friedman and Christiansen

"Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy" by David Corfield (just took this one to OBX North Carolina to enjoy on my beach vacation last week! Got some salt water in those pages. Also speaks to Category Theory.)

For Category Theory:

"The Joy of Abstraction" (2023) by Euginia Cheng

"Basic Category Theory for Computer Scientists" by Benjamin C. Pierce

"Conceptual Mathematics: A first introduction to categories" by Lawvere and Schanuel

"Categories for the Working Philosopher" by Landry

https://youtu.be/atYp386EGo8

Should I upgrade my development and business workstation from Windows 10 to Linux (instead of upgrading to Windows 11)?

I'm extremely intimidated in taking the leap. I'm very familiar with Linux without a UI, and feel very comfortable with managing linux servers. I setup and run a cluster of RHEL servers for a private-cloud OpenStack deployment (kvm hypervisor). Familiar with apache web servers, and I run my own Asterisk PBX phone system, and have in the past done my own email server. Networking, iptables, etc.

But I've never used Linux in a desktop UI environment. Ever. Always been an MS Windows guy. But Windows 11?

I think my biggest fear are driver issues and having to convert a ton of files over to new formats for things I use to run my business. (Lots of MS Excel files for example). I use Microsoft Office (Word, Outlook, Excel) and Microsoft Visual Studio (F# Development) heavily. Excel is my biggest worry. And fighting with driver issues.

I'm familiar mostly with RHEL (CentOS, and I guess now "Rocky Linux").

Anyone here convert from Windows to Linux? What kind of issues did you run into? Should I do it?

Perhaps most importantly: Which Linux distro should I choose, and which desktop environment?

-AMD Ryzen Threadripper 2950X 16-Core 3.50 GHz

-Aorus X399 XTreme EATX TR4

-128GB RAM

-NVIDEO GeForce RTX 2080 (Gigabyte)

-(Two) 1TB NVMe Samsung SSD 970

Comments URL: https://news.ycombinator.com/item?id=29582490

Points: 9

# Comments: 10

How do you enforce required fields in the data model? By eliminating the possibility of null values, you eliminate the possibility of not-null constraints in the data model. I end up having to enforce these types of (non-complex) constraints outside the relational model. A missing row is not detectable in the same way as a null column value.

The reason... I like seeing how different languages handle asynchronous code vs synchronous code. F# has their way, C# has theirs, JavaScript async/await, colored functions, Project Loom, co-routines, React Fibers, etc. I'm intrigued that a language that has built-in algebraic effects can do async wihtout any other changes to the language (as if async and sync were the same).

Is there any relation to defunctionalization for this kind of stuff?

Philip Wadler had this to say about the paper: "Certain papers change your life. McCarthy's 'Recursive Functions of Symbolic Expressions and their Computation by Machine (Part I)' (1960) changed mine, and so did Landin's 'The Next 700 Programming Languages' (1966). And I remember the moment, halfway through my graduate career, when Guy Steele handed me Reynolds's 'Definitional Interpreters for Higher-Order Programming Languages' (1972)."[2] This is how I discovered it I believe.

The paper is exceedingly approachable. It was so well written that I immediately purchased a used copy of Reynolds' book on programming languages (which I did not have as easy time with compared to the paper - and still remains unfinished on my bookshelf).

When they republished the paper in 1998, Reynolds wrote about how the paper came to be [3], and I believe about the discoveries of continuations [4].

I recently implemented Reynold's meta-circular interpreter in TypeScript and serialized the abstract syntax into JSON. Coincidentally, a few days later I saw a post on HN something about "executable JSON" or some such "programming language" that the creator was very proud of making it into a product of sorts. (found it... JSON Logic: https://news.ycombinator.com/item?id=27306263). Queue Greenspun's tenth rule. I chuckled as I looked at the JSON Logic syntax knowing that a little Reynold's interpreter with its AST serialized to JSON is infinitely more powerful and extensible (allowing higher-order functions and such). I highly recommend anyone reading this to write the 50 or so lines of TypeScript necessary to implement Reynold's meta-circular interpreter (EXTREMELY EASY and nearly identical line-for-line to the 1998 paper, only in TypeScript instead of lambda calculus).

Good stuff.

[0] [PDF] https://surface.syr.edu/cgi/viewcontent.cgi?article=1012&con...

[1] [PDF] https://homepages.inf.ed.ac.uk/wadler/papers/papers-we-love/...

[2] https://homepages.inf.ed.ac.uk/wadler/topics/history.html#de...

[3] [PDF] https://homepages.inf.ed.ac.uk/wadler/papers/papers-we-love/...

[4] [PDF] https://homepages.inf.ed.ac.uk/wadler/papers/papers-we-love/...

Comments URL: https://news.ycombinator.com/item?id=28078181

Points: 2

# Comments: 0

Particularly the part of getting logically-consistent results via different routes of computation. David Kohn says this in the blog post: "But, you have to have in-depth (and sometimes rather arcane) knowledge about each aggregate’s internals to know which ones meet the above criteria – and therefore, which ones you can re-aggregate."

I think Giarrusso addresses the internal requirements in a precise mathematical manner (though I may be wrong). Giarrusso Section 2.1 is the specific area I'm thinking, particularly Definition 2.1 and then later the discussion of the abelian group where certain binary operations must be commutative and associative. Giarrusso Equation 1 in the introducton defines externally what it means to be logically consistent.

Also, Giarrusso talks about "Self-Maintainability" where updating the continuous result only needs to look at the changes to the input. What was obvious to me from reading Giarrusso was that something simple like "AVG" is not self-maintainable unless you keep the intermediate state (sum and count) seperately. Kohn's distinction of Transition Function, Combine Function, and Final Function - together with Giarrusso's abelian group and change structure - is kind of a big deal in making arbitrary functions "continuous"-capable while being "self-maintainable".

I can see designing a [data] structure that adheres to the specific algabraic laws defined by Giarrusso's abelian group along with the 3 functions from Kohn (missing from Giarrusso). You can then feed this structure to a function that spits out two new functions for you: a normal function that can be used to calculate a result, and it's "continuous" version which only needs change to the inputs. For example, "avg()" and "avg_continuous()" can be automatically derived from a data structure of algebraically well-behaved operations.

Plus this would have a really cool Category Theory diagram for it!

David: absolutely love the animated gifs and pictures. Very well written indeed.

[0] Giarrusso et. al. https://www.researchgate.net/publication/269126515_A_theory_...

Apple HQ - around 1,600ft diameter

Seneca Pumped Storage Lake: around 2,400ft diameter

This is exactly the feeling I had when visiting the Seneca Pumped Storage Generating Station that I mentioned in one of my other comments that I just posted before seeing your post. Truly awe inspiring. (Links provided in my other comment). Do go visit one of these!

They pump water up to it at night (when there is excess energy in the power grid), and let the water out in the day when the demand for energy is high (turning some turbines on its way down).

Prior to visiting I had an intellectual understanding of the concept of pumped storage [1], but I have to admit that it's one heck of an experience when you see it up close and personal. My thoughts standing at the edge of this massively perfect-circle deep lake full of water: "somebody built that... and it's one BIG BATTERY".

If you get a chance to visit one of these, I highly recommend it!

[0] https://en.wikipedia.org/wiki/Seneca_Pumped_Storage_Generati...

[1] https://en.wikipedia.org/wiki/Pumped-storage_hydroelectricit...

[0] Scott Wlaschin "Functional programming design patterns" https://vimeo.com/113588389

[Edit] Spoiler alert: each of the design patterns reviewed and contrasted in the video I mentioned seemed to "disappear" in FP since the equivalent is simply to use functions and/or function composition. Recently transitioning from C# to F# for my .NET Core projects, I felt the "glue code" the author mentions disappear in a similar manner with greatly-reduced code bloat.

Every interaction our human minds have with fiveness is with a representation or encoding of 5. With each new representation, I’ve experienced fiveness slightly differently.

But I like computers and math. For me, the best to experience oneness with the fiveness is through computation with Lambda Calculus and Church Numerals. Very fond of that encoding.

It's based on Haskell's Parsec parser combinator library, and is zero-dependency.

I was convinced to give it a try based on watching the author's YouTube videos "Parser Combinators From Scratch" on "Low Level JavaScript". Enjoyable series - recommended.

But then I was able to re-start Thompson's "Type Theory and Functional Programming" and it was clear that I started to understand a lot of it.

If you enjoy the nostalgia of older books like me, then pick up an original copy of "Intuitionistic Type Theory" edited by Per Martin-Löf.