Haskell

cross-posted from: https://kbin.social/m/haskell/t/552503

News about the Haskell programming language from 2023-10-19.

cross-posted from: https://kbin.social/m/haskell/t/533616

News about the Haskell programming language from 2023-10-12.

New-ish to Haskell. Can't figure out the best way to get Cassava (Data.Csv) to do what I want. Can't tell if I'm missing some haskell type idioms or common knowledge or what.

Task: I need to read in a CSV, but I don't know what the headers/columns are going to be ahead of time. The user will provide input to say which headers from the CSV they want processed, but I won't know where (index-wise) those columns will be in the CSV, nor how many total columns there will be (either specified by the user or total). Say I have a [String] which lists the headers they want.

Cassava is able to read CSVs with and without headers.

Without headers Cassava can read in entire rows, even if it doesn't know how many columns are in that row. But then I wouldn't have the header data to filter for the values that I need.

With headers Cassava requires(?) you to define a record type instantiating its FromNamedRecord typeclass, which is how you access parts of the column by name (using the record fields). But in order for this to be well defined you need to know ahead of time everything about the headers: their names, their quantity, and their order. You then emulate that in your record type.

Hopefully I'm missing something obvious, but it feels a lot like I have my hands tied behind my back dealing with the types provided by Cassava.

Help greatly appreciated :)

cross-posted from: https://infosec.pub/post/3538345

Found on Mastodon. NOT crypto.

Utilizing Functional Reactive Programming, FRP - with the reactive-banana Library to create a terminal animation using termbox-banana.

cross-posted from: https://infosec.pub/post/2175721

Abstract. Formal languages are commonly used to model the seman- tics of instruction set architectures (e.g. ARM). The majority of prior work on these formal languages focuses on concrete instruction execu- tion and validation tasks. We present a novel Haskell-based modelling approach which allows the creation of flexible and versatile architecture models based on free monads and a custom expression language. Con- trary to existing work, our approach does not make any assumptions regarding the representation of memory and register values. This way, we can implement non-concrete software analysis techniques (e.g. sym- bolic execution where values are SMT expressions) on top of our model as interpreters for this model. In contrast to prior work, our modelling approach is therefore explicitly focused on the creation of custom ISA in- terpreters. We employ our outlined approach to create an abstract model and a concrete interpreter for the RISC-V base instruction set. Based on this model, we demonstrate that custom interpreters can be implemented with minimal effort using dynamic information flow tracking as a case study.

Answering the question raised at the end of Part 1, we take a look at how a hypothetical Strict Haskell would tie the compilers hands despite pervasive purity. We also examine how laziness permits optimizations that come with no intrinsic cost and compare its benefits to a strict language with opt-in laziness.

Part 1:

• Laziness in Haskell — Part 1: Prologue
Series Playlist:

• Laziness in Haskell

— Contact: • Tweag Website: https://www.tweag.io/ • Tweag Twitter: https://twitter.com/tweagio • Alexis King's Twitter: https://twitter.com/lexi_lambda

We teach you Haskell

I listen to this (now very old) episode often to get inspired.

When John starts talking about compiling to categories, at around 14:40 to around 30:00, it gets REALLY interesting.

*😁😁 Hoping to bring this kind of discussion to the new Formal Methods community. 😁😁 * Here's the work he talked about: Compiling to categories by Conal Elliott

I need someone to get into the weeds on compiling programs to "axiomatized closed categories". What are the implications? What are the ramifications?

Here's the conclusion of the paper Wadler is referring to in this interview:

Proposition as Types informs our view of the universality of certain programming languages. The Pioneer spaceship contains a plaque designed to communicate with aliens, if any should ever intercept it. They may find some parts of it easier to interpret than others. A radial diagram shows the distance of fourteen pulsars and the centre of the galaxy from Sol. Aliens are likely to determine that the length of each line is proportional to the distances to each body. Another diagram shows humans in front of a silhouette of Pioneer. If Star Trek gives an accurate conception of alien species, they may respond “They look just like us, except they lack pubic hair.” However, if the aliens’s perceptual system differs greatly from our own, they may be unable to decipher these squiggles. What would happen if we tried to communicate with aliens by transmitting a computer program? In the movie Independence Day, the heroes destroy the invading alien mother ship by infecting it with a computer virus. Close inspection of the transmitted program shows it contains curly braces—it is written in a dialect of C! It is unlikely that alien species would program in C, and unclear that aliens could decipher a program written in C if presented with one. What about lambda calculus? Propositions as Types tell us that lambda calculus is isomorphic to natural deduction. It seems difficult to conceive of alien beings that do not know the fundamentals of logic, and we might expect the problem of deciphering a program written in lambda calculus to be closer to the problem of understanding the radial diagram of pulsars than that of understanding the image of a man and a woman on the Pioneer plaque. We might be tempted to conclude that lambda calculus is universal, but first let’s ponder the suitability of the word ‘universal’. These days the multiple worlds interpretation of quantum physics is widely accepted. Scientists imagine that in different universes one might encounter different fundamental constants, such as the strength of gravity or the Planck constant. But easy as it may be to imagine a universe where gravity differs, it is difficult to conceive of a universe where fundamental rules of logic fail to apply. Natural deduction, and hence lambda calculus, should not only be known by aliens throughout our universe, but also throughout others. So we may conclude it would be a mistake to characterise lambda calculus as a universal language, because calling it universal would be too limiting.

A great talk by one of the greats to get the ball rolling in this new community.

This is a spot to chat about anything relating to the haskell programming language!

Currently this community doesn't have any mods so if you want to moderate it feel free to dm me or reply here