Pinned toot

Domain (business) logic is related to your type system usage. As a programmer, the less you use your type system, the more you have to keep the domain logic in your head. The domain logic in your head is like the global state: opaque, ever-changing and informal, i.e., something to minimise and avoid as much as possible. If there is a requirement to acquire a big global state before you delve into the code, you know the type system is used sparingly.

PeerTube v3: it’s a live, a liiiiive !

🎉🎉🎉 PeerTube v3 is out today!!! 🎉🎉🎉

On the blog :
➡️ The stages of development
➡️ Peer to peer live streaming
➡️ A behind-the-scenes short film
➡️ What we imagine for the future!

framablog.org/2021/01/06/peert

Illus CC-By @davidrevoy

Can you see the numbers in their silhouettes?
Here is my illustration to wish the end of the pandemic for 2021. Let's hope it will happen.
Happy New Year!
#krita

On empirically comparing two different software implementations: "Short of doubling our staff
and implementing it a second time, it is impossible to precisely measure the change in productivity,
prevalence of bugs, or altered user experience compared to the counterfactual situation where
fancy type system features were instead avoided." ~ doi.org/10.1145/3341704

Even if this parallel universe was possible, the comparison would be questionable because of their dependence.

In , how to define an instance of Data.Serialize (from cereal) for a GADT? Say I have:

data GIndex = One | Two
data MySum (ix :: GIndex) where
A :: Int -> MySum 'One
B :: Bool -> MySum 'Two

How to define the get method from the type class Serialize for the MySum type constructor?

An easy case for total (strong) functional programming: make your functions total so that you don't have to come up with inevitably unreliable heuristics for killing a potentially long-running data processing function.

Static typing is about scalability: the bigger and more complex your computer system becomes, the harder it gets to for us humans to keep guaranteeing it behaves as expected. Humans cannot possibly check all the features, neither can they do that for all feature interactions, as the interactions grow rapidly and exponentially in numbers. The time that humans can invest in checking doesn't scale. What does scale is machine time, and static typing uses machine time effectively.

Here is a classical and recurring example of a failure to use a type system to encode a piece of the domain logic. An optional value of one type makes sense on its own and another optional value of another type also makes sense on its own. However, when both are present in a product type, not all four combinations always make sense. One should use a sum type with as many data constructors as there are meaningful combinations in the domain, but obviously less than four.

I am very excited to announce the 2020 State of #Haskell Survey! Please take 10 minutes to fill it out. Thanks! haskellweekly.news/survey/2020

777 Books sold since the release two weeks ago! Thank you! 🎉 I hope you'll get the geek joke.( I'm not worrying a lot on Mastodon 😇 ). My 'Special Launch Offer' sale ends on Saturday 31, in three days. Will it reach 1000? That would be amazing. Last chance to get them while they're cheap!
davidrevoy.com/shop

Domain (business) logic is related to your type system usage. As a programmer, the less you use your type system, the more you have to keep the domain logic in your head. The domain logic in your head is like the global state: opaque, ever-changing and informal, i.e., something to minimise and avoid as much as possible. If there is a requirement to acquire a big global state before you delve into the code, you know the type system is used sparingly.

Isn't it perplexing to see someone eagerly writing raw SQL when they could have used a type-safe embedded domain-specific language such as Esqueleto in Haskell? Why does anyone want to give up on composability and bug-checking?

It is funny to see people using fallacies such as assuming the conclusion. For example, when arguing about the best of multiple options, if one is left without arguments to support their choice, they can say one should use the right tool for the right job, thereby trying to imply their choice is the right tool. After all, who is against using the right tool for the right job?

A yet another Yesod rant: I introduced bugs into a code base because I wasn't aware of mandatory presence of two request headers that I should have validated values of. Hence, instead of me encoding this requirement via Haskell's type system (the Servant framework empowers you to do so), incidentally I had others waste time in fixing bugs I have grown.

Do you remember those times when medicine ‘professionals’ refused the idea of hand washing?
We are in this very phase when software ‘professionals’ refuse to use proper type systems.

And "nothing" is what you get under 1201. When the RIAA complains about youtube-dl to Github, Github pulls it down, but if the developers counternotify them, Github can't restore the files without facing CRIMINAL liability (5 years/$500k).

15/

Show thread

Thanks to @debian 's €10,000 donation (and not $10,000 as announced a few hours ago), we've just reached the 4th step of our PeerTube fundraising. Many thanks to all those who donated. And it's not too late to contribute : joinpeertube.org/roadmap

I'm excited to see my proposal for a different formalisation of de Bruijn indices merged into a book Programming Language Foundations in Agda (authors: Wadler, Kokke, Siek)!

github.com/plfa/plfa.github.io

The new formalisation is based on proof by reflection instead of relying on postulates and partial functions.

Total functional programming and dependent types rock!

To install a language extension for (including Haskell's language server protocol implementation called Haskell Language Server):

codium --install-extension haskell.haskell

It finally looks like there is a Haskell IDE I can recommend to others! (I just have to turn a blind eye to the fact it is implemented in .)

Show thread

I didn't realize there is a binary distribution of VSCode named !

vscodium.com/

Hence there is no need to use proprietary VSCode or Atom for that matter. Unlike VSCode, VSCodium does not track you and report on your editor usage to the headquarters in Redmond. To make things even better, it comes with its own extension repository hosting only free software extensions:

open-vsx.org/

Show older
La Quadrature du Net - Mastodon - Media Fédéré

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!