diff --git a/doc/manual/Makefile b/doc/manual/Makefile new file mode 100644 index 00000000..9107bf99 --- /dev/null +++ b/doc/manual/Makefile @@ -0,0 +1,5 @@ +watch: + ./typst.sh watch haskus.typ + +compile: + ./typst.sh compile haskus.typ diff --git a/doc/manual/fonts/ShareTechMono-Regular.ttf b/doc/manual/fonts/ShareTechMono-Regular.ttf new file mode 100644 index 00000000..0ae0b197 Binary files /dev/null and b/doc/manual/fonts/ShareTechMono-Regular.ttf differ diff --git a/doc/manual/fonts/neo-sans/Neo Sans Std Black Italic.otf b/doc/manual/fonts/neo-sans/Neo Sans Std Black Italic.otf new file mode 100644 index 00000000..1414ce4c Binary files /dev/null and b/doc/manual/fonts/neo-sans/Neo Sans Std Black Italic.otf differ diff --git a/doc/manual/fonts/neo-sans/Neo Sans Std Black.otf b/doc/manual/fonts/neo-sans/Neo Sans Std Black.otf new file mode 100644 index 00000000..8226d8e7 Binary files /dev/null and b/doc/manual/fonts/neo-sans/Neo Sans Std Black.otf differ diff --git a/doc/manual/fonts/neo-sans/Neo Sans Std Bold Italic.otf b/doc/manual/fonts/neo-sans/Neo Sans Std Bold Italic.otf new file mode 100644 index 00000000..18aa09ca Binary files /dev/null and b/doc/manual/fonts/neo-sans/Neo Sans Std Bold Italic.otf differ diff --git a/doc/manual/fonts/neo-sans/Neo Sans Std Bold.otf b/doc/manual/fonts/neo-sans/Neo Sans Std Bold.otf new file mode 100644 index 00000000..77f2f6cf Binary files /dev/null and b/doc/manual/fonts/neo-sans/Neo Sans Std Bold.otf differ diff --git a/doc/manual/fonts/neo-sans/Neo Sans Std Italic.otf b/doc/manual/fonts/neo-sans/Neo Sans Std Italic.otf new file mode 100644 index 00000000..b85f90a8 Binary files /dev/null and b/doc/manual/fonts/neo-sans/Neo Sans Std Italic.otf differ diff --git a/doc/manual/fonts/neo-sans/Neo Sans Std Light Italic.otf b/doc/manual/fonts/neo-sans/Neo Sans Std Light Italic.otf new file mode 100644 index 00000000..f102a13e Binary files /dev/null and b/doc/manual/fonts/neo-sans/Neo Sans Std Light Italic.otf differ diff --git a/doc/manual/fonts/neo-sans/Neo Sans Std Light.otf b/doc/manual/fonts/neo-sans/Neo Sans Std Light.otf new file mode 100644 index 00000000..81cfb8e7 Binary files /dev/null and b/doc/manual/fonts/neo-sans/Neo Sans Std Light.otf differ diff --git a/doc/manual/fonts/neo-sans/Neo Sans Std Medium Italic.otf b/doc/manual/fonts/neo-sans/Neo Sans Std Medium Italic.otf new file mode 100644 index 00000000..ff28641f Binary files /dev/null and b/doc/manual/fonts/neo-sans/Neo Sans Std Medium Italic.otf differ diff --git a/doc/manual/fonts/neo-sans/Neo Sans Std Medium.otf b/doc/manual/fonts/neo-sans/Neo Sans Std Medium.otf new file mode 100644 index 00000000..2f528df2 Binary files /dev/null and b/doc/manual/fonts/neo-sans/Neo Sans Std Medium.otf differ diff --git a/doc/manual/fonts/neo-sans/Neo Sans Std Regular.otf b/doc/manual/fonts/neo-sans/Neo Sans Std Regular.otf new file mode 100644 index 00000000..496752f6 Binary files /dev/null and b/doc/manual/fonts/neo-sans/Neo Sans Std Regular.otf differ diff --git a/doc/manual/fonts/neo-sans/Neo Sans Std Ultra Italic.otf b/doc/manual/fonts/neo-sans/Neo Sans Std Ultra Italic.otf new file mode 100644 index 00000000..6a382132 Binary files /dev/null and b/doc/manual/fonts/neo-sans/Neo Sans Std Ultra Italic.otf differ diff --git a/doc/manual/fonts/neo-sans/Neo Sans Std Ultra.otf b/doc/manual/fonts/neo-sans/Neo Sans Std Ultra.otf new file mode 100644 index 00000000..49a2a94c Binary files /dev/null and b/doc/manual/fonts/neo-sans/Neo Sans Std Ultra.otf differ diff --git a/doc/manual/fonts/uwch.ttf b/doc/manual/fonts/uwch.ttf new file mode 100644 index 00000000..5581ff6d Binary files /dev/null and b/doc/manual/fonts/uwch.ttf differ diff --git a/doc/manual/haskus.typ b/doc/manual/haskus.typ new file mode 100644 index 00000000..83720fcd --- /dev/null +++ b/doc/manual/haskus.typ @@ -0,0 +1,92 @@ +#set text(font: "Neo Sans Std") + +#set heading(numbering: "1.1.1.1 ") +#show heading: it => { + set text( + weight: "medium" + , rgb("#0860a8") + , font: "Share Tech Mono" + ) + v(8pt) + it +} + +// Page break before level 1 titles +#show heading.where(level:1): it => { + pagebreak(weak: true) + it +} + +#show raw.where(block: true): it => block( + fill: rgb("#fae1df") + , inset: 8pt + , radius: 5pt + , text(fill: rgb("#1c2826"), it) +) + +#show raw.where(block: false): it => highlight( + fill: rgb("#fae1df") + , text(fill: rgb("#1c2826"), it) +) + +// Palette: +// 0680A8 (blue) +// D64550 (red) +// FAE1DF (rose) +// 1C2826 (black) +// CFFFE5 (green) + +#set document( + title: "Haskus packages manual" + , author: "Sylvain Henry" + , date: auto +) + +#set page( + numbering: "1" + , number-align: right +) + +// Front page + +#page( + numbering: none, + align(center, + [ + #v(40%) + #text( + size: 26pt, + [ + Haskus Computer Manual + ] + )\ + #v(5%) + #text( + size: 22pt, + [ + Sylvain Henry + ] + ) + #v(5%) + #text( + size: 12pt, + [ + Version: #datetime.today().display() + ] + ) + ] + ) +) + +#outline() + +#include "src/intro.typ" +#include "src/stdlib.typ" +#include "src/system.typ" +#include "src/compiler.typ" +#include "src/graphics.typ" + +#bibliography( + style: "ieee", + "src/biblio.yml" + ) diff --git a/doc/manual/images/logo.png b/doc/manual/images/logo.png new file mode 100644 index 00000000..5dbf722a Binary files /dev/null and b/doc/manual/images/logo.png differ diff --git a/doc/manual/src/biblio.yml b/doc/manual/src/biblio.yml new file mode 100644 index 00000000..6a0aacb7 --- /dev/null +++ b/doc/manual/src/biblio.yml @@ -0,0 +1,8 @@ +linux-initramfs: + type: Web + title: initramfs buffer format + author: + - Al Viro + - H. Peter Anvin + date: 2002-01-13 + url: https://www.kernel.org/doc/html/latest/driver-api/early-userspace/buffer-format.html diff --git a/doc/manual/src/compiler.typ b/doc/manual/src/compiler.typ new file mode 100644 index 00000000..c0c7e61f --- /dev/null +++ b/doc/manual/src/compiler.typ @@ -0,0 +1,3 @@ += Compilers + +#include "compiler/x86.typ" diff --git a/doc/manual/src/compiler/images/x86-encoding.svg b/doc/manual/src/compiler/images/x86-encoding.svg new file mode 100644 index 00000000..d3c09455 --- /dev/null +++ b/doc/manual/src/compiler/images/x86-encoding.svg @@ -0,0 +1,2850 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + + Legacy prefixes + 66 + 67 + 2E + 3E + 26 + 64 + 65 + 36 + F0 + F3 + F2 + + } G1 + } G2 + } G4 + + } + + + + + + + + + G5 + + } + + + + + + + + G3 + + + CS descriptor + L flag + D/B flag + + + + + + + + + EFLAGS + VM flag + + + + + + CR0 + PE flag + + + + + + IA32_EFER + LMA flag + + Mode + M + Legacy Real + Legacy Virtual 8086 + Legacy Protected + Long Compatibility + Long 64-bit + 0 + 1 + 2 + 3 + 4 + + + CS.D/B + M + 0 + 1 + 2 + 3 + 4 + + + + PE + LMA + 0 + 1 + 1 + 1 + 0 + 0 + 1 + 1 + + + + + 1 + 0 + + VM + 0 + 1 + 0 + 0 + 0 + + + L + X + X + 0 + 1 + 0 + + + + + + + + + + + Must be zero + + Default operationsize (DOS) + Default addresssize (DAS) + + + X + X + 0 + 1 + 0 + 1 + 0 + 3 + 2 + 16-bit + 32-bit + 64-bit + 16-bit + 16-bit + 16-bit + 16-bit + 16-bit + 32-bit + 16-bit + 16-bit + 32-bit + 32-bit + 32-bit + + + Must be zero + + Overriden operationsize (OOS) + DOS + 66 + 32-bit + 16-bit + 16-bit + 32-bit + 0 + 0 + 1 + 1 + 32-bit + 16-bit + 32-bit + 16-bit + + + + + + + Overriden addresssize (OAS) + DAS + 67 + 32-bit + 16-bit + 16-bit + 32-bit + 0 + 0 + 1 + 1 + 32-bit + 16-bit + 32-bit + 16-bit + + + + + + + 64-bit + 0 + 64-bit + 64-bit + 1 + 32-bit + + + Prefixes + W + + + + + + D/B flag + SS descriptor + + + + SS.D/B + M + 0 + 1 + 2 + 3 + 4 + + + + Default stacksize (DSS) + X + X + 0 + 1 + 0 + 1 + 0 + 3 + 2 + 16-bit + 32-bit + 16-bit + 16-bit + 16-bit + 32-bit + 64-bit + + + + + W + Instruction defaults to64-bit operation Size + Overriden OperationSize 64 (OOS64) + * + 1 + 0 + 64-bit + 0 + OOS + 1 + 0 + 64-bit + + + + + + diff --git a/doc/manual/src/compiler/x86.typ b/doc/manual/src/compiler/x86.typ new file mode 100644 index 00000000..e683add2 --- /dev/null +++ b/doc/manual/src/compiler/x86.typ @@ -0,0 +1,105 @@ +== x86 assembly + +Notes on x86 in ``haskus-system`` and in general. + +=== Instruction list + +`haskus-system` aims to support X86 architectures by providing a declarative +list of instruction specifications (in `Haskus.Arch.X86_64.ISA.Insns.`) that +can be used to write: + +- disassemblers +- assemblers +- analyzers +- (micro-)benchmarks +- emulators/simulators + +Most instruction lists I have found (e.g., NASM's insns.dat file, Intel's +documentation) "flatten" the instruction polymorphism down to operand classes: +for each instruction, there is an entry in the list for each tuple of possible +operand classes. In ``haskus-system``, I have tried to keep as much of the +original semantics in a declarative way. For instance, I describe the semantics +of some optional bits in the opcodes: + +- bit indicating that operands have to be commuted +- bit indicating that the operand size is 8-bit +- bit indicating that the FPU stack is popped +- etc. + +In theory, it should be easily possible to generate a flattened instruction list +from `haskus-system`'s one, while the other way around is much more involved. + +Additionally, the list contains for each instruction: + +- flags that are read/set/unset/undefined +- implicit operands +- operand access mode: Read/Write/Both/None (used to access metadata) +- constraints: alignment requirement for memory +- supported prefixes +- required X86 extensions +- some documentation + +In the future, I would like to add: + +- pseudo-code for each instruction (useful for emulators, etc.) +- exceptions (maybe inferred from pseudo-code?) +- required privileges +- maybe precomputed latencies and such as found in Agner's work + (http://www.agner.org) for different architectures (useful for + cross-compilers) and a way to compute them ourselves on the current + architecture + +=== Instruction Operands + +The polymorphism of x86 instructions is hard to formalize. For each operand, we +have to consider: + +- the type of data it represents: an integer, a float, a vector of something +- its size +- where it is stored: in memory or in a register (which depends on the type and + size) + +There are often functional dependencies between operands: the type of one of the +operands may constrain the type of the other ones. + +Usually assemblers infer the operand size from the operands, but as memory +addresses don't indicate the type of the data they point to, explicit +annotations are sometimes required. + +=== Semantics vs Encoding + +There isn't an isomorphism between an instruction and its encoding. Put another +way: sometimes it is possible to encode a given instruction using different +encodings. A basic example is to add superfluous prefixes (e.g., overriding the +default segment with the same segment). The semantics of the program stays the +same but there are side-effects: + +- instruction size vs instruction cache +- instruction alignment vs instruction decoder + +An assembler would have to choose whether to use one encoding form or another. +In ``haskus-system``, I have tried to define an isomorphism between instruction +encodings and a more high-level instruction description by using encoding +variants (see ``EncodingVariant`` in ``Haskus.Arch.X86_64.ISA.Insn``). The +decoder indicates which variant of an instruction encoding it has decoded. The +(future) encoder will allow the user to specify which encoding to use (for +side-effect considerations). + +=== Instruction entry point + +x86 ISA uses some prefixes to alter the meaning of some instructions. In the +binary form (in the legacy encoding), a prefix is just a byte put before the +rest of the instruction bits. + +It is possible to jump/branch into the instruction *after* some prefixes in +order to avoid them. Hence there is a kind of instruction overlay: two +"different" instructions sharing some bits in the binary. It makes the +representation and the analyze of these programs a little bit trickier. +Especially if we make a non-linear disassembly by following branchs: we get +branch labels inside instructions. + +I have been told this is used in the glibc. + +=== Encoding size + +#image("images/x86-encoding.svg") diff --git a/doc/manual/src/graphics.typ b/doc/manual/src/graphics.typ new file mode 100644 index 00000000..be6330be --- /dev/null +++ b/doc/manual/src/graphics.typ @@ -0,0 +1,250 @@ += Computer Graphics + +Computer Graphics is a vast topic. It encompasses most visual things we use a +computer for: + +- image digitalization: what is a digital image and how do we store it +- image compression: how to compress digital images (with or without loss of + information +- image printing +- image display: video display technologies +- image processing: transforming images +- image analysis and computer vision: analyzing images +- image generation: generating images from a formal description (ray-tracing, etc.) +- image editing: providing interactive user interfaces for image manipulation + using virtual tools + +If you're already a programmer, it's very likely that you've already read about +RGB colors: with just three numbers (quantity of red, quantity of green, +quantity of blue), we can describe any color (for example on a web page). If +you're curious you may ask yourself: how is that possible? Why red, green, and +blue? Are there other colors that can't be represented with this triplet? + +These are all valid questions. In this book we don't skim over the explanations +about the physics of light and the biology of our light sensors (our eyes). +These information are required for other topics such as image compression and +physically-based image generation (e.g. photon mapping). + +Be warned that if you go too deep into this rabbit-hole, you'll quickly +encounter quantum mechanics and get out with even more questions than you +started with. + +== The physics of light + +It so happens that our world is surrounded by *electromagnetic radiations* and +they are important for our topic because some of them are what we call "light". + +Electromagnetic radiations are produced by the Sun, by fire, by lamps, by +microwave ovens, etc. They travel through space: in vacuum, in the air, to some +degree into water, glass and other materials. They can bounce on surfaces +(objects, people, particles...) or be absorbed by them. Ultimately some of them +may reach our eyes. Some cells in our eyes react to some particular +electromagnetic radiations and transmit signals to our brain that are +interpreted as colors. + +#figure( + caption: "A painting depicting some electromagnetic radiations from the Sun", + image( + width: 60%, + "graphics/images/sunset.png" + ) +) + +In physics there are two common models to describe electromagnetic radiations, +their travels and their interactions: +- at our scale, we can use the model of *electromagnetic waves* +- at the atomic scale, *quantum electrodynamics* (with photon particles) is a + better model + +=== Electromagnetic waves + +The speed of an electromagnetic radiation is determined by the medium/material +it is in. In vacuum, this speed is 299,792,458 m/s (the well known "speed of +light" constant, denoted with $c_0$). $c_0$ is the upper limit for the speed of an +electromagnetic radiation. + +TODO: optical frequency $v$ is constant for a monochromatic wave. +https://www.rp-photonics.com/wavelength.html + +To avoid manipulating large speed numbers, the speed $v$ in other materials is +often given with the *refractive index* $n$ of the material, defined as: $n = +c_0/v$ + + +#table( + columns: (auto, auto, auto), + align: (left,center,right), + table.header( + [*Material*], [*Refractive index $n$*], [*Phase velocity (m/s)* $v$] + ), + [Vacuum], [1], [299,792,458], + [Glass], [1,5], [\~200,000,000], +) + + + + +=== Human Vision + + +Video display technology is based on human vision in several ways: + +*Color perception* + +The human eye uses 3 kinds of sensors (in daylight) called +#link("https://en.wikipedia.org/wiki/Cone_cell")[cones] , each covering some +part of the #link("https://en.wikipedia.org/wiki/Visible_spectrum")[visible +spectrum]. Their behavior is quite complicated because their response ranges +overlap, the count of each sensor differs, the light perception is non-linear, +etc. For the human eye, different +#link("https://en.wikipedia.org/wiki/Spectral_power_distribution")[spectral +power distributions] can lead to the same perceived color +#link("https://en.wikipedia.org/wiki/Metamerism_(color)")[metamerism] . + +Long story short, a video display doesn't have to be able to produce every +frequency of the visible spectrum to reproduce colors: it just has to produce 3 +of them to trigger each kind of cone at a different level. Typically a video +display produces color by combining different amount of red, green and blue +lights which roughly correspond to each cone response peak. + +Usually video display devices can only produce a subset of the visible color +space (or #link("https://en.wikipedia.org/wiki/Gamut")[gamut]). + +*Spatial integration* + +If several lights of different colors are emitted very closely to each other, +our eyes can't distinguish them and we don't perceive the gap between them. +Instead we only perceive another color which is composed of the emitted ones. + +Screens display an array of lights called pixels (say 1920x1080 pixels) which +are very close one to the other so that we perceive a continuous picture without +distinguishing the gaps between each pixel individually (at normal viewing +distance of the video display). + +Screens display pixel themselves as a combination of several (at least 3 but +sometimes more) distinct lights (red, green and blue) which are so close that we +perceive them as a single color. + + +*Temporal integration* + +Similarly to the spatial integration, our eyes cannot distinguish lights that +change too fast over time. Instead we perceive an integration of the light over +time. + +Screens use this to simulate continuous motion: if different images are +displayed very quickly, our eyes don't distinguish each picture individually. +Some video displays even emit a single line of pixels at a time or a single pixel +at a time, or alternate between even and odd lines for each frame. + +Note that our peripheral vision is better at detecting motion. It explains why +virtual reality (VR) headsets have higher refresh rates. + +*Summary* + +Rendering an image on a video display surface consists in indicating the color +of each pixel. Note that pixels are samples of the image we would like to render +on the video display surface if it had an infinite resolution, +#link("http://alvyray.com/Memos/CG/Microsoft/6_pixel.pdf")[not "small squares"]. + +We have to render many different images per seconds to simulate moving images. + +I recommend watching this video: +#link("https://www.youtube.com/watch?v=3BJU2drrtCM")[How a TV works in slow +motion] + + +=== Video Display + +A video display usually shows a rectangle of pixels. When connected to a +computer, it is managed by a graphics chipset which indicates to the video +display the color of each pixel of the current image to show several times per +second. + +The algorithm used by the graphics chipset is roughly: + +``` +For each pixel in the current image + Read its color from memory + Convert the color into something intelligible for the video display + Send the converted pixel color to the video display + +Wait until it's time to send the next image (vertical blanking interval) +``` + +==== Refresh rates + +The number of images (or frames) sent to the video display depends on its +refresh rate. Most video displays have a fixed (configurable) refresh rate. For +instance 60Hz (60 frames per second). + +Newer video displays may also support variable refresh rates where the delay +between two frames may depend on the next frame being ready (or a timeout if it +isn't ready for too long). + +==== Switching between frames + +If we modify the memory containing the pixel colors while the graphics chipset +is reading it, the video display may show incoherent pixels (e.g. pixels from +two different frames). This is called *tearing*. We usually want to avoid it. + +The idea is to modify the pixel colors only while the graphics chipset is +waiting between two transfers. For historical reasons this period of time is +called the +#link("https://en.wikipedia.org/wiki/Vertical_blanking_interval")[vertical +blanking interval (VBI or VBLANK)]. + +If the software can't render a frame fast enough during the VBI, we usually want +the previous frame to be sent again. In order to do that, we use two buffers +(*double-buffering*): one buffer contains the current frame that is sent +repeatedly to the video display and the other contains the frame the software is +currently rendering. Once the next frame is ready we only have to switch the +buffer pointer (called *page-flipping*) during the VBI to inverse the roles of +the two buffers. + +If the software renders frames too fast we can either block it until +page-flipping occurs or we can use *triple-buffering*: one buffer contains the +current frame as before, the second contains a pending frame (if any) which is a +frame ready to be displayed, and the third one contains the frame being rendered +as before. When the rendering in the third buffer is done, there is a switch +between the second and the third buffer (i.e. one of the rendered frame may not +be displayed at all if there was already a pending frame). During the VBI, if +there is a pending frame in the second buffer, there is a switch between the +first and the second buffers. + +==== Plane composition + +Instead of using a single source for the pixel colors, some graphics chipsets +allow the use of several pixel sources that are blended/composed together. + +A *plane* describes a portion of the video display surface that uses a specific +source of pixel colors. Basic graphics chipsets only have a single primary plane +that occupies the whole video display surface; other graphics chipsets may have +several other planes with different properties (pixel formats, dimensions, +rotation, scaling, etc.). + +This is particularly useful for what is called *hardware cursor*. A small cursor +plane is dedicated to display the mouse cursor so when the mouse moves we only +have to change the position of the cursor plane independently of the other +planes. It makes the cursor much more responsive because this operation is very +cheap. + +Planes can also be used to render hardware decoded videos, overlays, etc. + +*Summary* + +The graphics chipset sends the pixel colors from the memory to the connected +video display several times per second (depending on the refresh rate). + +The graphics chipset supports at least one primary plane but it can also support +additional planes (overlay, cursor, etc.) with additional properties (scaling, +rotation, different pixel format, etc.). + +The software is responsible of producing pixel colors for each plane. To avoid +tearing, the switch from one frame to the other must be done during the vertical +blanking interval (VBI or VBLANK). Double- or triple-buffering can be used for +this purpose. + +== Further reading + +- The Computer Graphics Manual (David Salomon) diff --git a/doc/manual/src/graphics/images/sunset.png b/doc/manual/src/graphics/images/sunset.png new file mode 100644 index 00000000..d17e585f Binary files /dev/null and b/doc/manual/src/graphics/images/sunset.png differ diff --git a/doc/manual/src/helpers.typ b/doc/manual/src/helpers.typ new file mode 100644 index 00000000..66532179 --- /dev/null +++ b/doc/manual/src/helpers.typ @@ -0,0 +1,8 @@ +#let trivia(x) = block( + fill: rgb("#fae1df") + , inset: 8pt + , radius: 5pt + , text(fill: rgb("#1c2826"), x) +) + + diff --git a/doc/manual/src/intro.typ b/doc/manual/src/intro.typ new file mode 100644 index 00000000..66134b99 --- /dev/null +++ b/doc/manual/src/intro.typ @@ -0,0 +1,4 @@ += Introduction + +The Haskus Computer Manual is a book in several volumes about computer +programming. diff --git a/doc/manual/src/stdlib.typ b/doc/manual/src/stdlib.typ new file mode 100644 index 00000000..e40b3af3 --- /dev/null +++ b/doc/manual/src/stdlib.typ @@ -0,0 +1,11 @@ +#import "helpers.typ" as haskus + += Programming in Haskell + +The Haskus standard library is a set of Haskell modules. It provides support for +some common data structures. + +#include "stdlib/numbers.typ" +#include "stdlib/variant.typ" +#include "stdlib/eadt.typ" +#include "stdlib/binary.typ" diff --git a/doc/manual/src/stdlib/binary.typ b/doc/manual/src/stdlib/binary.typ new file mode 100644 index 00000000..f8660ab5 --- /dev/null +++ b/doc/manual/src/stdlib/binary.typ @@ -0,0 +1,1017 @@ +== Data representation + +``haskus-binary`` is a package containing a set of modules dedicated to the +manipulation of binary data. It also provides data type mapping those of other +languages such as C and even more. + +Some packages (e.g. ``haskus-system``) use these binary modules to provide +bindings to C libraries. We don't want to rely on external tools such as C2HS to +provide bindings to C libraries because: + +- We don't want to depend on .h files; +- .h files often contain pecularities that are difficult to handle + automatically; +- Documentation and code of the resulting Haskell files are often very bad: + + - No haddock + - Very low-level (e.g. `#define` are not transformed into ADTs with Enum + instances) + +Instead ``haskus-binary`` lets you write bindings in pure Haskell code and +provides many useful things to make this process easy. + +=== Word, Int + +`Haskus.Format.Binary.Word` contains data types representing unsigned words +(`Word8`, `Word16`, `Word32`, etc.) and signed integers (`Int8`, `Int16`, +`Int32`, etc.). It also contains some C types such as `CSize`, `CShort`, +`CUShort`, `CLong`, `CULong`, etc. + +==== Endianness + +Words and Ints are stored (i.e., read and written) using host endianness (byte +ordering). `AsBigEndian` and `AsLittleEndian` data types in the +`Haskus.Format.Binary.Endianness` module allow you to force a different +endianness. + +The following example shows a data type containing a field for each endianness +variant. We explain how to use this kind of data type as a C structure later in +this document. + +```haskell +data Dummy = Dummy + { fieldX :: Word32 -- ^ 32-byte unsigned word (host endianness) + , fieldY :: AsBigEndian Word32 -- ^ 32-byte unsigned word (big-endian) + , fieldZ :: AsLittleEndian Word32 -- ^ 32-byte unsigned word (little-endian) + } + deriving (Generic,Storable) +``` + +We can also explicitly change the endianness with the following methods: +`hostToBigEndian`, `hostToLittleEndian`, `bigEndianToHost`, +`littleEndianToHost`, `reverseBytes`. + +Each of these methods is either equivalent to `id` or to `reverseBytes` +depending on the host endianness. + +=== Structures (records) + +You map C data structures with Haskell data type as follows: + +```haskell +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} + +import Haskus.Format.Binary.Storable +import Haskus.Utils.Types.Generics (Generic) + +data StructX = StructX + { xField0 :: Word8 + , xField1 :: Word64 + } + deriving (Show,Generic,Storable) +``` + + +The Storable instance handles the alignment of the field as a C non-packed +structure would (i.e. there are 7 padding bytes between `xField0` and +`xField1`). + +`peek` and `poke` can be used to read and write the data structure in memory. + +==== Nesting + +Data structures can be nested: + +```haskell +data StructY = StructY + { yField0 :: StructX + , yField1 :: Word64 + } + deriving (Show,Generic,Storable) +``` + +=== Arrays (vectors) + +`haskus-binary` supports vectors: a fixed amount of Storable data correctly +aligned. You can define a vector as follows: + +```haskell +{-# LANGUAGE DataKinds #-} + +import Haskus.Format.Binary.Vector as V + +v :: Vector 5 Word16 +``` + +Vectors are storable, so you can `peek` and `poke` them from memory. +Alternatively, you can create them from a list: + +```haskell +Just v = fromList [1,2,3,4,5] +Just v = fromList [1,2,3,4,5,6] -- this fails dynamically +Just v = fromList [1,2,3,4] -- this fails dynamically + +-- take at most 5 elements then fill with 0: v = [1,2,3,4,5] +v = fromFilledList 0 [1,2,3,4,5,6] + +-- take at most 5 elements then fill with 7: v = [1,2,3,7,7] +v = fromFilledList 7 [1,2,3] + +-- take at most 4 (!) elements then fill with 0: v = [1,2,3,0,0] +v = fromFilledListZ 0 [1,2,3] + +-- useful for zero-terminal strings: s = "too long \NUL" +s :: Vector 10 CChar +s = fromFilledListZ 0 (fmap castCharToCChar "too long string") +``` + +You can concatenate several vectors into a single one: + +```haskell +import Haskus.Utils.HList + +x = fromFilledList 0 [1,2,3,4] :: Vector 4 Int +y = fromFilledList 0 [5,6] :: Vector 2 Int +z = fromFilledList 0 [7,8,9] :: Vector 3 Int + +v = V.concat (x `HCons` y `HCons` z `HCons` HNil) + +>:t v +v :: Vector 9 Int + +> v +fromList [1,2,3,4,5,6,7,8,9] +``` + +You can also safely `drop` or `take` elements in a vector. You can also `index` +into a vector: + +```haskell +import Haskus.Format.Binary.Vector as V + +v :: Vector 5 Int +v = fromFilledList 0 [1,2,3,4,5,6] + +-- v2 = [1,2] +v2 = V.take @2 v + +-- won't compile (8 > 5) +v2 = V.take @8 v + +-- v2 = [3,4,5] +v2 = V.drop @2 v + +-- x = 3 +x = V.index @2 v +``` + +Finally, you can obtain a list of the values + +```haskell +> V.toList v +[1,2,3,4,5] +``` + +=== Enums + +If you have a C enum (or a set of `#define`'s) with consecutive values and +starting from 0, you can do: + +```haskell +{-# LANGUAGE DeriveAnyClass #-} + +import Haskus.Format.Binary.Enum + +data MyEnum + = MyEnumX + | MyEnumY + | MyEnumZ + deriving (Show,Eq,Enum,CEnum) +``` + +If the values are not consecutive or don't start from 0, you can write your own +`CEnum` instance: + +```haskell +-- Add 1 to the enum number to get the valid value +instance CEnum MyEnum where + fromCEnum = (+1) . fromIntegral . fromEnum + toCEnum = toEnum . (\x -> x-1) . fromIntegral +``` + +To use an Enum as a field in a structure, use `EnumField`: + +```haskell +data StructZ = StructZ + { zField0 :: StructX + , zField1 :: EnumField Word32 MyEnum + } + deriving (Show,Generic,Storable) +``` + +The first type parameter of `EnumField` indicates the backing word type (i.e. the +size of the field in the structure). For instance, you can use Word8, Word16, +Word32 and Word64. + +To create or extract an `EnumField`, use the methods: + +```haskell +fromEnumField :: CEnum a => EnumField b a -> a +toEnumField :: CEnum a => a -> EnumField b a +``` + +We use a CEnum class that is very similar to Enum because Enum is a special +class that has access to data constructor tags. If we redefine Enum, we cannot +use `fromEnum` to get the data constructor tag. + + +=== Bit sets (or "flags") + +We often use flags that are combined in a single word. Each flag is associated +to a bit of the word: if the bit is set the flag is active, otherwise the flag +isn't active. + +`haskus-binary` uses the `CBitSet` class to get the bit offset of each flag. By +default, it uses the Enum instance to get the bit offsets as in the following +example: + +```haskell +{-# LANGUAGE DeriveAnyClass #-} + +import Haskus.Format.Binary.BitSet + +data Flag + = FlagX -- bit 0 + | FlagY -- bit 1 + | FlagZ -- bit 2 + deriving (Show,Eq,Enum,CBitSet) +``` + +If you want to use different bit offsets, you can define your own CBitSet +instance: + +```haskell +-- Add 1 to the enum number to get the valid bit offset +instance CBitSet Flag where + toBitOffset = (+1) . fromEnum + fromBitOffset = toEnum . (\x -> x-1) +``` + +To use a bit set as a field in a structure, use BitSet: + +```haskell +data StructZ = StructZ + { zField0 :: ... + , zField1 :: BitSet Word32 Flag + } + deriving (Show,Generic,Storable) +``` + +The first type parameter of BitSet indicates the backing word type (i.e. the +size of the field in the structure). For instance, you can use Word8, Word16, +Word32 and Word64. + +Use the following methods to manipulate the BitSet: + +```haskell +fromBits :: (CBitSet a, FiniteBits b) => b -> BitSet b a +toBits :: (CBitSet a, FiniteBits b) => BitSet b a -> b +member :: (CBitSet a, FiniteBits b) => BitSet b a -> a -> Bool +notMember :: (CBitSet a, FiniteBits b) => BitSet b a -> a -> Bool +toList :: (CBitSet a, FiniteBits b) => BitSet b a -> [a] +fromList :: (CBitSet a, FiniteBits b, Foldable m) => m a -> BitSet b a +intersection :: FiniteBits b => BitSet b a -> BitSet b a -> BitSet b a +union :: FiniteBits b => BitSet b a -> BitSet b a -> BitSet b a +``` + +Note that we don't check if bit offsets are outside of the backing word. You +have to choose a backing word that is large enough. + + +=== Unions + +An union provides several ways to access the same buffer of memory. To use them +with `haskus-binary`, you need to give the list of available representations +in a type as follows: + +```haskell +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DataKinds #-} + +import Haskus.Format.Binary.Union + +u :: Union [Word8, Word64, Vector 5 Word16] +``` + +Unions are storable so you can use them as fields in storable structures or +you can directly `peek`/`poke` them. + +You can retrieve a member of the union with `fromUnion`. The extracted type +must be a member of the union otherwise it won't compile. + +```haskell +fromUnion u :: Word64 +fromUnion u :: Word8 +fromUnion u :: Vector 5 Word16 +fromUnion u :: Word32 -- won't compile! +``` + +To create a new union from one of its member, use `toUnion` or `toUnionZero`. +The latter sets the remaining bytes of the buffer to 0. In the example, the +union uses 10 bytes (`5 * 2` for `Vector 5 Word16`) and we write 8 bytes +(`sizeOf Word64`) hence there are two bytes that can be left uninitialized +(`toUnion`) or set to 0 (`toUnionZero`). + +```haskell +u :: Union [Word8,Word64,Vector 5 Word16] +u = toUnion (0x1122334455667788 :: Word64) + +> print (fromUnion u :: Vector 5 Word16) +fromList [30600,21862,13124,4386,49850] + +-- or +u = toUnionZero (0x1122334455667788 :: Word64) +> print (fromUnion u :: Vector 5 Word16) +fromList [30600,21862,13124,4386,0] +``` + + +=== Bit fields + +You may need to define bit fields over words. For instance, you can +have a Word16 split into 3 fields X, Y and Z composed of 5, 9 and 2 bits +respectively. + +#table( + columns: (auto, auto, auto, auto), + table.header( + [], [*X*], [*Y*], [*Z*] + ), + [`w :: Word16`], + [0 0 0 0 0], + [0 0 0 0 0 0 0 0 0], + [0 0], +) + +You define it as follows: + +```haskell +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeApplications #-} + +import Haskus.Format.Binary.BitField + +w :: BitFields Word16 [ BitField 5 "X" Word8 + , BitField 9 "Y" Word16 + , BitField 2 "Z" Word8 + ] +w = BitFields 0x0102 +``` + +Note that each field has its own associated type (e.g. Word8 for X and Z) +that must be large enough to hold the number of bits for the field. + +Operations on BitFields expect that the cumulated size of the fields is equal +to the whole word size: use a padding field if necessary. + +You can extract and update the value of a field by its name: + +```haskell +x = extractField @"X" w +z = extractField @"Z" w +w' = updateField @"Y" 0x100 w +-- w' = 0x402 + +z = extractField @"XXX" w -- won't compile + +w'' = withField @"Y" (+2) w +``` + +Fields can also be `BitSet` or `EnumField`: + +```haskell +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveAnyClass #-} + +import Haskus.Format.Binary.BitField +import Haskus.Format.Binary.Enum +import Haskus.Format.Binary.BitSet + +data A = A0 | A1 | A2 | A3 deriving (Show,Enum,CEnum) + +data B = B0 | B1 deriving (Show,Enum,CBitSet) + +w :: BitFields Word16 [ BitField 5 "X" (EnumField Word8 A) + , BitField 9 "Y" Word16 + , BitField 2 "Z" (BitSet Word8 B) + ] +w = BitFields 0x1503 +``` + +BitFields are storable and can be used in storable structures. + +You can easily pattern-match on all the fields at the same time with +`matchFields` and `matchNamedFields`. It creates a tuple containing one value +(and its name with `matchNamedFields`) per field. + +```haskell +> matchFields w +(EnumField A2,320,fromList [B0,B1]) + +> matchNamedFields w +(("X",EnumField A2),("Y",320),("Z",fromList [B0,B1])) +``` + +== Explicit Memory Management + +This document is about explicit ("manual") memory management in Haskell. It +starts from the very low level memory allocation and buffer management and then +builds up to "pointer" management, binary writer/reader monads, binary +serialization of Haskell data, large file mapping, embedding of large binary +blobs into applications, etc. + +=== Introduction + +==== Rationale + +Haskell is a garbage-collected language and is known for its use of immutable +data: why would we like to manage memory explicitly? Here is a list of reasons: + +1. Support for large data sets +2. Close to the metal: better control and usually faster operations +3. Interaction with the outside world +4. Live outside of the garbage-collector (no GC overhead) + +==== Memory model + +The memory model we consider is the +#link("https://en.wikipedia.org/wiki/Flat_memory_model")[flat memory model]. A +memory is an array of cells each containing one *bit*. A bit is a binary digit +(either 0 or 1). Instead of indexing each bit individually, the memory is +divided in coarser groups of bits. Nowadays most architectures pack bits in +groups of 8 bits (called "byte" or "Word8" in Haskell) so that's what we assume. + +Consecutive bytes are assigned consecutive addresses: an *address* is a number +(starting from 0) which maximal value depends on the architectures. For example, +on X86_64 architectures an address is stored in a 64-bit word but only the 48 +lower bits are used. + +Even if the whole memory is addressable, some addresses can't be given as +parameters to reading/writing instructions depending on the execution context +(state of the memory, state of the processes, etc.). Otherwise an +error/exception/interruption may be triggered or the result may be undefined. + +This memory model is abstract: it can be applied to physical memory or to +virtual memory managed by some software (operating systems, system libraries, +etc.). + +==== Memory allocation + +Nowadays most mainstream systems and architectures require the use of a memory +allocator. Applications can't just read or write random addresses in memory +otherwise it could lead to data corruption or to prohibited access errors. +Instead programs must reclaim a chunk of consecutive cells (i.e. a +*buffer*) to the memory allocator. + +Note: a memory allocator is also abstract: its facilities can be provided by the +hardware (less common), by the operating system (usually not used directly) or +by some "system libraries" built on the the operating system allocator (most +common). + +The memory allocator tries to find a suitable set of consecutive memory cells +that fulfills the given constraints (minimal number of cells, address constraints +such as alignment or maximal value, etc.). It makes sure that these cells are +now accessible to the calling code and returns the address of the first cell to +the calling code. + +Programs can release buffers that are no longer used. Memory cells of released +buffers can be used by the memory allocator for future memory allocations. + +Allocating and releasing buffers can lead to memory +#link("https://en.wikipedia.org/wiki/Fragmentation_(computing)")[fragmentation]: +there are enough free memory cells to allocate but these are not consecutive +because allocated memory cells are still alive between them. + +==== GHC memory allocation + +GHC provides its own memory allocator on top of the system one. It is well +integrated with the copying garbage collector. + +The main difference with the system one is that there is an additional +indirection: instead of returning the address of the first allocated memory +cell, GHC's memory allocator returns an abstract object that contains a mutable +memory address. GHC can freely copy the contents of the buffer to another +location and update the address in the abstract object. This avoids +fragmentation at the cost of buffer copying. + +As copying buffers can be too costly, GHC's memory allocator also supports the +allocation of *pinned* buffers: these buffers are guaranteed not to be moved, +exactly like system allocated buffers. As an optimization, GHC automatically +considers large buffers as pinned buffers. + +GHC also distinguishes at the type level buffers whose cells are mutable or +immutable. Immutable buffers can be shared, duplicated at will, etc. Mutable +buffers are cheaper to use as we don't have to duplicate the whole buffer to +change one cell as it would be the case with immutable buffers. Immutable +buffers are created by "freezing" mutable buffers: by convention a frozen +mutable buffer mustn't be used anymore (linear types may help to ensure this +statically in the future). + +GHC allocated buffers are automatically released by the garbage collector. + +Note: memory allocation in GHC is done with `MutableByteArray#` and `ByteArray#` +data types and their primitives. + +// ============================================================================== +// State of the art +// ============================================================================== +// +// State of the art as of January 14, 2019. +// +// * Data.ByteString.Short: +// ShortByteString ~ BufferI +// +// * Data.ByteString.Strict: +// ByteString ~ BufferSlice ({-# UNPACK #-} !BufferP) +// +// +// * ByteString: misleading name (not a textual string). Especially because of +// Data.ByteString.Char8.{pack/unpack} +// +// +// * Data.ByteString.Lazy: BufferList BufferP +// Lazy IO: quite bad +// Fixed chunck size +// +// * ByteString: embedding as literal strings (slow, don't support \0 in the +// buffer) +// +// * ByteArray, MutableByteArray +// +// * Ptr, ForeignPtr: don't track buffer size + +=== Buffer + +A `Buffer` object represents some allocated memory, i.e. a set of consecutive +memory cells. It has the following type: + +```haskell +data Buffer (mut :: Mutability) (pin :: Pinning) (fin :: Finalization) (heap :: Heap) +``` + +It's a GADT whose parameters have the following meaning: + +```haskell +-- | Is the buffer mutable or not? +data Mutability + = Mutable -- ^ Memory cells are mutable + | Immutable -- ^ Memory cells are immutable + +-- | Is the buffer pinned into memory? +data Pinning + = Pinned -- ^ The buffer has a fixed associated memory address + | NotPinned -- ^ The buffer contents can be freely moved to another address + +-- | Is the buffer automatically garbage collected? +data Finalization + = Collected -- ^ Automatically collected by the garbage-collector + | Finalized -- ^ Finalizers are run just before GCing + | NotFinalized -- ^ Not managed at all + +-- | Allocation heap +data Heap + = Internal -- ^ GHC heap + | External -- ^ External heap +``` + +If you have read the sections about memory allocation in general (@memory-alloc) +and memory allocation in GHC (@memory-alloc-ghc), most parameters must be self +explanatory, except for `Finalized` explained below (@buffer-finalizer). + +We define the following type aliases for the different buffer variants: + +```haskell +type BufferI = Buffer 'Immutable 'NotPinned 'Collected 'Internal +type BufferP = Buffer 'Immutable 'Pinned 'Collected 'Internal +type BufferM = Buffer 'Mutable 'NotPinned 'Collected 'Internal +type BufferMP = Buffer 'Mutable 'Pinned 'Collected 'Internal +type BufferME = Buffer 'Mutable 'Pinned 'NotFinalized 'External +type BufferE = Buffer 'Immutable 'Pinned 'NotFinalized 'External +type BufferF = Buffer 'Immutable 'NotPinned 'Finalized 'Internal +type BufferPF = Buffer 'Immutable 'Pinned 'Finalized 'Internal +type BufferMF = Buffer 'Mutable 'NotPinned 'Finalized 'Internal +type BufferMPF = Buffer 'Mutable 'Pinned 'Finalized 'Internal +type BufferMEF = Buffer 'Mutable 'Pinned 'Finalized 'External +type BufferEF = Buffer 'Immutable 'Pinned 'Finalized 'External +``` + +==== Buffer size + +Buffer size can be queried with: + +```haskell +bufferSizeIO :: MonadIO m => Buffer mut pin fin heap -> m Word +bufferSize :: BufferSize a => a -> Word +``` + +`bufferSize` is pure and as such it can't be used with internal mutable buffers +which can be resized. All the other buffers provide a `BufferSize` instance. + + +==== Finalizers + +A finalizer is just a side-effecting function that can be associated to a data. +When a data is to be collected by GHC's garbage collector, GHC executes its +associated finalizers if the data has some before releasing the data. This +mechanism is especially useful in the domain of explicit memory management (e.g. +to release externally allocated memory), hence `Buffers` can be `Finalized` +to ease the use of this mechanism. In particular it ensures execution order of +the finalizers by explicitly storing them in a list. + +We can make any buffer `Finalized` with the following function (idempotent for +already `Finalized` buffers): + +```haskell +makeFinalizable :: MonadIO m => Buffer mut pin f heap -> m (Buffer mut pin 'Finalized heap) +``` + +Then you can attach a finalizer with: + +```haskell +addFinalizer :: MonadIO m => Buffer mut pin 'Finalized heap -> IO () -> m () +``` + +The latest added finalizers are executed first. Note that finalizers are not +guaranteed to run (e.g. if the program exits before the buffer is collected). + +==== Allocation + +===== Allocation in GHC heap + +Buffers allocated in GHC heap can be pinned or not. They are automatically +collected. + +```haskell +newBuffer :: MonadIO m => Word -> m BufferM +newPinnedBuffer :: MonadIO m => Word -> m BufferMP +newAlignedPinnedBuffer :: MonadIO m => Word -> Word -> m BufferMP +``` + +`newAlignedPinnedBuffer` takes an additional alignement requirement. + +===== Allocation using system malloc + +Buffers allocated by system "malloc" allocator are pinned and must be either +explicitly freed with `Malloc.freeBuffer` or can be automatically freed by a +finalizer (e.g. if they are allocated with `Malloc.newFinalizedBuffer`). + +```haskell +import qualified Haskus.Memory.Allocator.Malloc as Malloc + +Malloc.newBuffer :: MonadIO m => Word -> m (Maybe BufferME) +Malloc.newFinalizedBuffer :: MonadIO m => Word -> m (Maybe BufferMEF) +Malloc.freeBuffer :: MonadIO m => BufferME -> m () +``` + +===== Buffer freezing/thawing + +Some buffers can be converted from mutable to immutable and vice versa. This is +unsafe as the original buffer mustn't be used anymore after this and this is not +statically checked by the compiler. + +```haskell +-- | Mutable to immutable +unsafeBufferFreeze :: (Freezable a b, MonadIO m) => a -> m b + +-- | Immutable to mutable +unsafeBufferThaw :: (Thawable a b , MonadIO m) => a -> m b +``` + +==== Read/write + +Several primitives are provided to read and to write buffer contents. Some +primitives have constraints on the buffer type to restrict their use. For +example, the type system ensures that we don't use writing primitives with +immutable buffers. + +===== Reading/writing Word8 + +We can read a `Word8` value by providing an index/offset into the buffer: + +```haskell +bufferReadWord8IO :: MonadIO m => Buffer mut pin fin heap -> Word -> m Word8 +``` + +This is done in the IO monad because the function is generic and supports both +mutable and immutable buffers. If we deal with immutable buffers, we can use the +following pure function instead: + +```haskell +bufferReadWord8 :: Buffer 'Immutable pin fin heap -> Word -> Word8 +``` + +We can also write `Word8` into mutable buffers with: + +```haskell +bufferWriteWord8IO :: MonadIO m => Buffer 'Mutable pin fin heap -> Word -> Word8 -> m () +``` + +===== Reading/writing Word16/Word32/Word64 + +Reading and writing `Word16`, `Word32` or `Word64` could be expressed with +the primitives to read/write `Word8`. However, most architectures provide +instructions to directly read/write larger words. Using them is much more +efficient than falling back to `Word8` primitives. Hence buffers support the +following primitives too: + +```haskell +bufferReadWord16 :: Buffer 'Immutable pin fin heap -> Word -> Word16 +bufferReadWord32 :: Buffer 'Immutable pin fin heap -> Word -> Word32 +bufferReadWord64 :: Buffer 'Immutable pin fin heap -> Word -> Word64 + +bufferReadWord16IO :: MonadIO m => Buffer mut pin fin heap -> Word -> m Word16 +bufferReadWord32IO :: MonadIO m => Buffer mut pin fin heap -> Word -> m Word32 +bufferReadWord64IO :: MonadIO m => Buffer mut pin fin heap -> Word -> m Word64 + +bufferWriteWord16IO :: MonadIO m => Buffer 'Mutable pin fin heap -> Word -> Word16 -> m () +bufferWriteWord32IO :: MonadIO m => Buffer 'Mutable pin fin heap -> Word -> Word32 -> m () +bufferWriteWord64IO :: MonadIO m => Buffer 'Mutable pin fin heap -> Word -> Word64 -> m () +``` + +Different architectures store the `Word8` s composing larger words in different +orders (called `Endianness`). When we use buffers to exchange data with other +systems, we need to be aware of the endianness convention used for the exchanged +data. More on this in the following chapters. + +===== Using the address of pinned buffers + +Pinned buffers have a fixed associated memory address. We can use the following +functions to read or write a mutable pinned buffer by using primitives for +`Addr#` or `Ptr`: + +```haskell +withBufferAddr# :: MonadIO m => Buffer 'Mutable 'Pinned fin heap -> (Addr# -> m a) -> m a +withBufferPtr :: MonadIO m => Buffer 'Mutable 'Pinned fin heap -> (Ptr b -> m a) -> m a +``` + +Similarly we can do the same thing with immutable buffers with the following +functions: + +```haskell +unsafeWithBufferAddr# :: MonadIO m => Buffer mut 'Pinned fin heap -> (Addr# -> m a) -> m a +unsafeWithBufferPtr :: MonadIO m => Buffer mut 'Pinned fin heap -> (Ptr b -> m a) -> m a +``` + +The difference in this case is that we mustn't use the memory writing primitives +of `Addr#` and `Ptr` when the buffer is immutable as it would break referential +transparency, hence the "unsafe" prefix. + +==== Copy + +We can copy data from one buffer to another with: + +```haskell +copyBuffer :: + MonadIO m + => Buffer mut pin0 fin0 heap0 -- ^ Source buffer + -> Word -- ^ Offset in source buffer + -> Buffer 'Mutable pin1 fin1 heap1 -- ^ Target buffer + -> Word -- ^ Offset in target buffer + -> Word -- ^ Number of Word8 to copy + -> m () +``` + +==== Performance + +To enhance performance of the code using `Buffer`, most functions have been +specialized with the `SPECIALIZE INLINE` pragma so that if your code uses a +specific buffer type (e.g. `BufferI`, `BufferM`...) it is as if the +generic `Buffer` GADT didn't exist. + +You can use it in your own generic code. Example: + +```haskell +{-# SPECIALIZE INLINE bufferReadWord8IO :: MonadIO m => BufferI -> Word -> m Word8 #-} +{-# SPECIALIZE INLINE bufferReadWord8IO :: MonadIO m => BufferP -> Word -> m Word8 #-} +``` + + +=== Literals and embedding + +Sometimes we know at compile time what the (initial) contents of a Buffer +(@buffer) is. It would be cumbersome to have to allocate the buffer and to write +its content word by word at program initialization or before using the buffer. +This chapter presents the alternatives. + +==== List literals + +If the buffer is very small, we can use the `OverloadedLists` extension to +create an immutable buffer from a list of bytes. It allows the creation of +small unpinned immutable buffers into GHC's heap (aka `BufferI`). + +```haskell +{-# LANGUAGE OverloadedLists #-} + +b :: BufferI +b = [25,26,27,28] -- Word8 values +``` + +This should only be used for very small buffers. First, because it is not the +most efficient way to build a buffer: the actual buffer will be created when it +is first used. Second, because it is very cumbersome to list bytes' values in a +list. + +=== Embedding files as buffers + +You can embed an external file (or some part of it) into your executable. At +runtime you can access it as a normal external buffer (mutable or not). + +```haskell +{-# LANGUAGE TemplateHaskell #-} + +import Haskus.Memory.Buffer +import Haskus.Memory.Embed + +let b = $(embedFile "myfile.bin" + True -- is the resulting buffer mutable or not + (Just 8) -- optional alignment constraint + (Just 10) -- optional offset in the file + (Just 128) -- optional number of bytes to include + ) +``` + +=== Embedding buffers using Template Haskell + +If you know how to build your buffer at compile time, you can build it and embed +it into the executable with Template Haskell by using `embedBuffer`. + +```haskell +import Haskus.Memory.Embed + +embedBuffer + :: Buffer mut pin fin heap -- ^ Source buffer + -> Bool -- ^ Should the embedded buffer be mutable or not + -> Maybe Word -- ^ Optional alignement constraint + -> Maybe Word -- ^ Optional offset in the source buffer + -> Maybe Word -- ^ Optional number of bytes to include + -> Q Exp -- ^ BufferE or BufferME, depending on mutability parameter +``` + +=== Views + +Views can be used to refer to a subset of the cells of a buffer. + +==== View patterns + +The cells referred by a view may not be contiguous. Currently we support the +following patterns: + +```haskell +-- | A view pattern +data ViewPattern + = PatternFull -- ^ The whole buffer + | Pattern1D -- ^ 1D slice + { pattern1DOffset :: {-# UNPACK #-} !Word -- ^ Offset of the first cell + , pattern1DSize :: {-# UNPACK #-} !Word -- ^ Number of cells + } + | Pattern2D -- ^ 2D slice + { pattern2DOffset :: {-# UNPACK #-} !Word -- ^ Offset of the first line + , pattern2DWidth :: {-# UNPACK #-} !Word -- ^ Width (line size) + , pattern2DHeight :: {-# UNPACK #-} !Word -- ^ Height (number of lines) + , pattern2DStride :: {-# UNPACK #-} !Word -- ^ Stride (space between two lines) + } + | PatternOn ViewPattern ViewPattern -- ^ Composed pattern +``` + +==== View sources + +A view can use one of the following sources: a (strong) buffer, a weak buffer or +a weak view. + +Strong views keep the underlying buffer alive, while weak views allow the source +to be garbage collected. + +1. The source is a buffer. The view keeps the buffer alive + +2. The source is a weak buffer. If the buffer is collected, its contents + is copied into a new buffer and the view is updated to use it. + +3. The source is a weak view. If the source view is collected, the + current view is updated to use whatever the source view uses as a + source (another view or a buffer). + This mechanism makes buffer contents cascade into smaller views while + preserving some sharing. + + +==== Weak views + +Weak views are used so that the underlying buffer can be freed by the GC. +When it happens and if the view is still alive the contents of the buffer +used by the view is copied into a fresh (usually smaller) buffer. + +Suppose we have a big buffer B. We can have buffer views on B, say vb1 and vb2. + +``` +B <----- vb1 +^------- vb2 +``` + +These views don't duplicate B's contents and they keep B alive. +If the views are much smaller than B, it may not be what we want: a lot of +space is wasted and we would better duplicate B's data required by the views +and free B. + +To support this, we can use "weak buffer views", say wbv1 and wbv2. + +``` +B <~~~~~ wbv1 +^~~~~~~~ wbv2 +``` + +If/when B is collected, new buffers are created from it for the views: + +``` +B1 <----- wbv1 +B2 <----- wbv2 +``` + +We can also create "weak view views", say wvv1 and wvv2: + +``` +B <~~~~~ wvb1 <~~~~~ wvv1 + ^~~~~~~~~ wvv2 +``` + +If/when B is collected before wvb1, the sharing is kept while the required +contents of B is duplicated: + +``` +B' <---- wbv1 <~~~~~ wvv1 + ^~~~~~~~~ wvv2 +``` + +When wbv1 is collected, we can be in one of the following state depending if +B has been collected already or not: + +``` +B <~~~~~~~~~~~~~~~~~ wvv1 +^~~~~~~~~~~~~~~~~~~~ wvv2 + + B' <~~~~~ wvv1 + ^~~~~~~~~ wvv2 +``` + +==== Example + +```haskell +> :set -XOverloadedLists +> import System.Mem +> v <- newBufferWeakView ([10,11,12,13,14,15,16,17] :: BufferI) (Pattern1D 2 4) +> v2 <- newViewWeakView v (Pattern1D 1 1) +> putStr =<< showViewState v2 +View source: weak view +Source size: 4 +View pattern: Pattern1D {pattern1DOffset = 1, pattern1DSize = 1} +Wasted space: 75% +Source: + View source: weak buffer + Source size: 8 + View pattern: Pattern1D {pattern1DOffset = 2, pattern1DSize = 4} + Wasted space: 50% + +> performGC + +> putStr =<< showViewState v2 +View source: weak view +Source size: 4 +View pattern: Pattern1D {pattern1DOffset = 1, pattern1DSize = 1} +Wasted space: 75% +Source: + View source: buffer -- the source of v (a weak buffer of size 8) has + Source size: 4 -- been replaced by a strong buffer of size 4 when + View pattern: PatternFull -- the source has been collected + Wasted space: 0% +``` + +```haskell +> v <- (`newViewWeakView` Pattern1D 1 2) =<< newBufferWeakView ([10,11,12,13,14,15,16,17] :: BufferI) (PatternFull) + +> putStr =<< showViewState v +Source size: 8 +View pattern: Pattern1D {pattern1DOffset = 1, pattern1DSize = 2} +Wasted space: 75% +Source: + View source: weak buffer + Source size: 8 + View pattern: PatternFull + Wasted space: 0% + +> performGC + +> putStr =<< showViewState v +View source: buffer +Source size: 2 +View pattern: PatternFull +Wasted space: 0% +``` diff --git a/doc/manual/src/stdlib/eadt.typ b/doc/manual/src/stdlib/eadt.typ new file mode 100644 index 00000000..cf125a0e --- /dev/null +++ b/doc/manual/src/stdlib/eadt.typ @@ -0,0 +1,1229 @@ + +== Extensible recursive ADTs (EADTs) + +EADTs are "extensible algebraic data types": they can be transformed (by adding +or removing constructors) and their constructors are not tied to a specific EADT +type, hence we can use them as constructors of different EADTs. + +EADT constructors and operations can be defined independently (even in different +modules) allowing a great modularity. As such there are an answer to the +"expression problem" (cf @eadt-background section). + +.. toctree:: + :maxdepth: 1 + :numbered: + + eadt/safe_pattern_matching + eadt/constructor_removal + eadt/constructor_split + eadt/background + +=== Introduction + +==== Motivating example + +Suppose we want to encode lambda-calculus using an ADT. We could use the +following one: + +```haskell +data Expr n -- "n" represents a variable name + = Lambda n (Expr n) + | Var n + | App (Expr n) (Expr n) +``` + +We can define a pretty-print operation: + +```haskell +prettyPrint :: Show n => Expr n -> String +prettyPrint = \case + Var n -> show n + Lambda n e -> mconcat ["\\",show n,".",prettyPrint e] + App e1 e2 -> mconcat ["(",prettyPrint e1,") (",prettyPrint e2,")"] +``` + +And we can test on an example: + +```haskell +sampleDouble :: Expr String +sampleDouble = Lambda "x" (Var "+" `App` Var "x" `App` Var "x") + +> putStrLn (prettyPrint sampleDouble) +\"x".(("+") ("x")) ("x") +``` + +Now suppose that we want to add support for annotations. We can define a new +expression ADT with an additional constructor: + +```haskell +data AExpr a n -- "n" represents a variable name, "a" represents an annotation + = ALambda n (AExpr a n) + | AVar n + | AApp (AExpr a n) (AExpr a n) + | Ann a (AExpr a n) +``` + +But now we need to rewrite our operations and expressions (such as "prettyPrint" +and "sampleDouble") to handle and to use the constructors of the new expression +ADT: + +```haskell +prettyPrintA :: (Show n, Show a) => AExpr a n -> String +prettyPrintA = \case + AVar n -> show n + ALambda n e -> mconcat ["\\",show n,".",prettyPrintA e] + AApp e1 e2 -> mconcat ["(",prettyPrintA e1,") (",prettyPrintA e2,")"] + Ann a e -> mconcat ["{",show a,"} ", prettyPrintA e] + + +sampleDoubleA :: AExpr a String +sampleDoubleA = ALambda "x" (AVar "+" `AApp` AVar "x" `AApp` AVar "x") + +sampleAnnA :: AExpr String String +sampleAnnA = Ann "Double its input" sampleDouble +``` + +Now the problem is that we have two totally independent expression types +(`Expr` and `AExpr`) with different operations (`prettyPrint` vs +`prettyPrintA`) which can't be easily mixed. Moreover to define +`prettyPrintA` we had to copy-paste `prettyPrint` just to add a single case +alternative. Now suppose that we want to add a new function (e.g. to compute +free variables of an expression): should we implement it for `Expr`, for +`AExpr`, for both? + +Finally suppose that we want to add some other constructors: we either get a +combinatorial explosion of ADTs and functions, or we give up on static checking +and use the "largest" ADT (which contains a superset of the constructors of the +others) with some conventions, e.g. comments and runtime assertions such as "at +this point this expression shouldn't contain any annotation" that are not +enforced by the compiler. + +==== Motivating example with EADTs + +The same example with EADTs would be written as follows. First we define the +EADTs: + +```haskell +import Haskus.Utils.EADT +import Haskus.Utils.EADT.TH + +data LambdaF n e = LambdaF n e deriving Functor +data VarF n e = VarF n deriving Functor +data AppF e = AppF e e deriving Functor +data AnnF a e = AnnF a e deriving Functor + +eadtPattern 'LambdaF "Lambda" +eadtPattern 'VarF "Var" +eadtPattern 'AppF "App" +eadtPattern 'AnnF "Ann" + +type Expr n = EADT [LambdaF n, VarF n, AppF] +type AExpr a n = EADT [LambdaF n, VarF n, AppF, AnnF a] +``` + +Then we define the `prettyPrint` operation by using type classes: + +```haskell +class PrettyPrint f where + prettyPrint' :: f String -> String + +instance Show n => PrettyPrint (VarF n) where + prettyPrint' (VarF n) = show n + +instance Show n => PrettyPrint (LambdaF n) where + prettyPrint' (LambdaF n e) = mconcat ["\\",show n,".",e] + +instance PrettyPrint AppF where + prettyPrint' (AppF e1 e2) = mconcat ["(",e1,") (",e2,")"] + +instance Show a => PrettyPrint (AnnF a) where + prettyPrint' (AnnF a e) = mconcat ["{",show a,"} ",e] + +prettyPrint :: BottomUp PrettyPrint xs String => EADT xs -> String +prettyPrint e = bottomUp (toBottomUp @PrettyPrint prettyPrint') e +``` + +We can test it with: + +```haskell +sampleDouble :: Expr String +sampleDouble = Lambda "x" (Var "+" `App` Var "x" `App` Var "x") + +sampleAnn :: AExpr String String +sampleAnn = Ann "Double its input" (liftEADT sampleDouble) + +> putStrLn (prettyPrint sampleDouble) +\"x".(("+") ("x")) ("x") + +> putStrLn (prettyPrint sampleAnn) +{"Double its input"} \"x".(("+") ("x")) ("x") +``` + +=== EADT basics + +EADTs can be found in the +#link("https://hackage.haskell.org/package/haskus-utils-variant")[haskus-utils-variant] +package. + +You need the following imports in your source: + +```haskell +import Haskus.Utils.EADT +import Haskus.Utils.EADT.TH -- template-haskell helpers +``` + +==== Defining constructors + +EADT constructors are data types that must have a `Functor` type-class instance. +Fortunately defining such data types is easy thanks to the `DeriveFunctor` +extension that automatically generates the Functor instance for us. + +For instance, let's define the constructors for a list: + +```haskell +{-# LANGUAGE DeriveFunctor #-} + +data ConsF a e = ConsF a e deriving (Functor) +data NilF e = NilF deriving (Functor) +``` + +Note that *both* data types are parameterised by `e` even if `e` isn't used +in `NilF` definition. + +==== Defining pattern synonyms + +We can match EADT values with the `VF` pattern synonym ("VF" stands for "Variant +Functor"). To make the use of EADTs more pleasant, it is highly recommended to +define an additional pattern synonym for each constructor: + +```haskell +pattern Cons :: ConsF a :<: xs => a -> EADT xs -> EADT xs +pattern Cons a l = VF (ConsF a l) + +pattern Nil :: NilF :<: xs => EADT xs +pattern Nil = VF NilF +``` + +These patterns hide the use of the `VF` pattern and make the code much easier +to work with. + +As this code is very straightforward to write, we provide Template-Haskell +helpers to generate them automatically. The previous patterns can be generated +with: + +```haskell +{-# LANGUAGE TemplateHaskell #-} + +import Haskus.Utils.EADT.TH + +eadtPattern 'ConsF "Cons" +eadtPattern 'NilF "Nil" +``` + +==== Defining the EADT + +An EADT is just a type alias as in the following `List` EADT example: + +```haskell +type List a = EADT [ConsF a, NilF] +``` + +==== Creating values + +Thanks to the pattern synonyms defined above, we can define values as we would +with a normal ADT: + +```haskell +strList :: List String +strList = Cons "How" (Cons "are" (Cons "you?" Nil)) +``` + +In some cases we have to help the type-checker to determine some types. For +instance, in the following example it can't infer the `a` type in `ConsF a`, +hence we have to use type ascriptions: + +```haskell +intList :: List Int +intList = Cons (10 :: Int) $ Cons (20 :: Int) $ Cons (30 :: Int) Nil +``` + +This is because the code is generic enough that the same pattern synonyms could +be used to build an heterogeneous list. For instance containing both `Int` and +`Float`: + +```haskell +mixedList :: EADT [ConsF Int, ConsF Float, NilF] +mixedList = Cons (10 :: Int) $ Cons (5.0 :: Float) $ Cons (30 :: Int) Nil +``` + +We could also easily define another pattern synonym when we work on `List` to +help the inference algorithm: + +```haskell +-- pattern for a specific EADT: List a +pattern ConsList :: a -> List a -> List a +pattern ConsList a l = Cons a l +``` + +We can see that when we use it we don't need type ascriptions because the +`Int` type is propagated: + +```haskell +intList :: List Int +intList = ConsList 10 $ ConsList 20 $ ConsList 30 Nil +``` + +==== Matching values + +It is easy and tempting to use the same pattern synonyms to match EADT values. +And indeed this works pretty well: + +```haskell +showEADTList :: Show a => List a -> String +showEADTList = \case + ConsList a l -> show a ++ " : " ++ showEADTList l + Nil -> "Nil" + _ -> undefined + +> putStrLn (showEADTList strList) +"How" : "are" : "you?" : Nil + +> putStrLn (showEADTList intList) +10 : 20 : 30 : Nil +``` + +However this approach is a unsatisfactory for two reasons: + + 1. The pattern matching isn't safe: for now the compiler cannot use the + EADT constructor type list to infer that the pattern-match is + complete. Hence we need the wildcard match to avoid a warning and to + use ``ConsList`` to help the type inference. A better alternative is + presented in the :ref:`safe pattern-matching + ` chapter. + + 2. The function isn't generic: if we would like to write a ``showEADTList`` + function that also works on the heterogeneous ``mixedList`` above or on + any future EADT provided its constructors can be handled, we need to + use another approach based on type-classes. This is presented in the + following chapters. + +=== Explicit recursive traversal + +When we need to traverse a data structure, we can either use predefined +traversal functions (e.g., `map`, `fold`, etc.) or write the recursive +function explicitly. EADTs are no different in this regard. + +In this chapter we explain how to write explicitly recursive functions for +EADTs: similarly to usual ADTs, it's better to use them only when generic +traversal functions (presented in following chapters) don't fit the bill. + +==== Traversal example + +If we were to write a `show` function for a list ADT, we could do it like +this: + +```haskell +data List a = Cons a (List a) | Nil + +showList :: Show a => List a -> String +showList = \case + Nil -> "Nil" + Cons a l -> show a ++ " : " ++ showList l +``` + +In `showList` we can pattern match on the constructors of `List a` because +the constructor list is closed. With EADTs the list of constructors isn't +closed and we want to be able to use the same code even with EADTs extended with +more constructors. To support this, we use type-classes to build the equivalent +of the `case` in `showList` above. + +Let's define a class `MyShow` that is very much like `Show` and that we will +use to print any EADT value: + +```haskell +class MyShow e where + myShow :: e -> String +``` + +We can define instances for the `List` constructors defined in a +previous chapter (@eadt-basics): + +```haskell +instance MyShow (NilF e) where + myShow _ = "Nil" + +instance (MyShow e, Show a) => MyShow (ConsF a e) where + myShow (ConsF a l) = show a ++ " : " ++ myShow l +``` + +Note how each instance corresponds to an alternative in `showList`. + + +It also requires some additional instances to traverse the `VariantF` +combinator datatype and the `EADT` recursivity handling datatype: + +```haskell +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE FlexibleInstances #-} + +instance MyShow (VariantF f (EADT f)) => MyShow (EADT f) where + {-# INLINE myShow #-} + myShow (EADT e) = myShow e + +instance MyShow (VariantF [] e) where + {-# INLINE myShow #-} + myShow = undefined + +instance + ( MyShow (f e) + , MyShow (VariantF fs e) + ) => MyShow (VariantF (f ': fs) e) + where + {-# INLINE myShow #-} + myShow v = case popVariantFHead v of + Right u -> myShow u + Left w -> myShow w +``` + +Note: this boilerplate code (hopefully always very similar and straightforward) +is the main reason you should strive to use predefined recursion schemes instead +of the explicit approach presented here. + +Note: the INLINE pragmas are used to ensure that in the generated code we get +the equivalent of the `case` expression in `showList`. + +Now we can test it: + +```haskell +strList :: List String +strList = Cons "How" (Cons "are" (Cons "you?" Nil)) + +intList :: List Int +intList = Cons (10 :: Int) $ Cons (20 :: Int) $ Cons (30 :: Int) Nil + +mixedList :: EADT [ConsF Int, ConsF Float, NilF] +mixedList = Cons (10 :: Int) $ Cons (5.0 :: Float) $ Cons (30 :: Int) Nil + +> putStrLn (myShow strList) +"How" : "are" : "you?" : Nil + +> putStrLn (myShow intList) +10 : 20 : 30 : Nil + +> putStrLn (myShow mixedList) +10 : 5.0 : 30 : Nil +``` + +==== Extension example + +If we add a new constructor, such as `NodeF` to build binary trees: + +```haskell +data NodeF a e = NodeF a e e deriving (Functor) + +eadtPattern 'NodeF "Node" +``` + +We can also add a `MyShow` instance for `NodeF`: + +```haskell +instance (MyShow e, Show a) => MyShow (NodeF a e) where + myShow (NodeF a l1 l2) = show a ++ "\n|- " ++ indent (myShow l1) + ++ "|- " ++ indent (myShow l2) + where + indent' [] = [] + indent' (x:xs) = x : fmap (" "++) xs + indent = unlines . indent' . lines +``` + +Now we can show binary trees as well as lists: + +```haskell +tree :: EADT [NodeF Int, NilF] +tree = Node (10 :: Int) + (Node (5 :: Int) Nil Nil) + (Node (30 :: Int) Nil Nil) + +> putStrLn (myShow tree) +10 +|- 5 + |- Nil + |- Nil +|- 30 + |- Nil + |- Nil +``` + +We can also mix up trees and lists by using `ConsF` and `NodeF` in the same +EADT: + +```haskell +mixedTree :: EADT [NodeF Int, ConsF Int, NilF] +mixedTree = Node (10 :: Int) + (Cons (5 :: Int) $ Cons (6 :: Int) $ Cons (7 :: Int) Nil) + (Node (30 :: Int) Nil Nil) + +> putStrLn (myShow mixedTree) +10 +|- 5 : 6 : 7 : Nil +|- 30 + |- Nil + |- Nil + +-- Note: the code to display trees isn't very clever so don't use it to +-- display list of trees. +``` + +=== Constraining constructors with `:<:` + +The `:<:` type operator is used to ensure that a constructor is present in an +EADT. For example if we consider the following type signature (that will be +developed in the example below): + +```haskell +distr :: (AddF :<: f, MulF :<: f) => EADT f -> Maybe (EADT f) +``` + +The constructors of `EADT f` are not specified but the constraints `(AddF :<: f, +MulF :<: f)` ensure that at least `AddF` and `MulF` constructors are present. + +Note that to shorten a list of constraints such as `(AddF :<: f, MulF :<: f)` +you can use the `:<<:` operator: `[AddF,MulF] :<<: f`. + +==== Transformation example + +Suppose we have the following EADT for arithmetic expressions: + +```haskell +{-# LANGUAGE DeriveFunctor #-} + +data ValF e = ValF Int deriving (Functor) +data AddF e = AddF e e deriving (Functor) +data MulF e = MulF e e deriving (Functor) + +eadtPattern 'ValF "Val" +eadtPattern 'AddF "Add" +eadtPattern 'MulF "Mul" + +type Expr = EADT [ValF, AddF, MulF] +``` + +We can define some value: + +```haskell +e1 :: Expr +e1 = Add (Val 10) + (Mul (Add (Val 5) + (Val 10)) + (Val 7)) +``` + +We can define instances of the `MyShow` class (defined in +@eadt-explicit-recursive): + +```haskell +instance MyShow (ValF e) where + myShow (ValF e) = show e + +instance MyShow e => MyShow (AddF e) where + myShow (AddF x y) = "(" ++ myShow x ++ " + " ++ myShow y ++ ")" + +instance MyShow e => MyShow (MulF e) where + myShow (MulF x y) = "(" ++ myShow x ++ " * " ++ myShow y ++ ")" + +> putStrLn (myShow e1) +(10 + ((5 + 10) * 7)) +``` + +Now we can define a transformation that distributes multiplication over +addition as follows: + +```haskell +-- distribute multiplication over addition if it matches +distr :: (AddF :<: f, MulF :<: f) => EADT f -> Maybe (EADT f) +distr (Mul a (Add c d)) = Just (Add (Mul a c) (Mul a d)) +distr (Mul (Add c d) a) = Just (Add (Mul c a) (Mul d a)) +distr _ = Nothing +``` + +Note that this function works on any EADT as long as it has `AddF` and +`MulF` constructors. We indicate such constraints with the `:<:` type +operator. + +Then we need a helper function that performs the traversal of the EADT: + +```haskell +import Control.Arrow ((>>>)) + +-- bottom up traversal that performs an additional bottom up traversal in +-- the transformed sub-tree when a transformation occurs. +bottomUpFixed :: Functor (VariantF cs) => (EADT cs -> Maybe (EADT cs)) -> EADT cs -> EADT cs +bottomUpFixed f = project >>> fmap (bottomUpFixed f) >>> embed >>> f' + where + f' u = case f u of + Nothing -> u + Just v -> bottomUpFixed f v + +-- | Distribute multiplication over addition +distribute :: ([AddF,MulF] :<<: cs) => EADT cs -> EADT cs +distribute = bottomUpFixed distr +``` + +Note: `bottomUpFixed` is a generic recursion scheme over an EADT. You can read +more on this approach in the dedicated chapter @eadt-recursion-schemes. + +Finally we can test the transformation on an example: + +```haskell +> putStrLn (myShow e1) +(10 + ((5 + 10) * 7)) + +> putStrLn (myShow (distribute e1)) +(10 + ((5 * 7) + (10 * 7))) +``` + +==== Extensibility + +Suppose we add a `Pow` (power) constructor: + +```haskell +data PowF e = PowF e e deriving (Functor) + +eadtPattern 'PowF "Pow" + +instance MyShow e => MyShow (PowF e) where + myShow (PowF x y) = "(" ++ myShow x ++ " ^ " ++ myShow y ++ ")" +``` + +We can now write expressions that use the `Pow` constructor: + +```haskell +type Expr2 = EADT [ValF, AddF, MulF, PowF] + +e2 :: Expr2 +e2 = Pow (Val 10) + (Mul (Add (Pow (Val 5) (Val 8)) + (Val 10)) + (Val 7)) +``` + +We can check that our distribution function still works on this new type of +expression without being modified at all: + +```haskell +> putStrLn (myShow (distribute e2)) +(10 ^ (((5 ^ 8) * 7) + (10 * 7))) +``` + +=== Recursion schemes and EADTs + +Traversing an EADT explicitly (see @eadt-explicit-recursive) can be +tedious. Another approach consists in using dedicated composable combinators +called *recursion schemes*. + +The well known `map` and `fold` functions are examples of recursion schemes +for lists: these functions handle the recursive traversal of the data structure +and are parameterized by the functions performing the actual work. Recursion +schemes are a generalization of this approach. + +The best introduction to recursion schemes I've read can be found here: +https://blog.sumtypeofway.com/an-introduction-to-recursion-schemes/ + +To avoid paraphrasing, I recommend that you read it before continuing. + +See also: https://bartoszmilewski.com/2013/06/10/understanding-f-algebras/ + +==== Catamorphism: Show example + +Suppose we rewrite our `Show` class like this: + +```haskell +class FunctorShow (f :: * -> *) where + functorShow :: f String -> String +``` + +We can define instances for `NilF` and `ConsF`: + +```haskell +instance FunctorShow NilF where + functorShow _ = "Nil" + +instance (Show a) => FunctorShow (ConsF a) where + functorShow (ConsF a l) = show a ++ " : " ++ l +``` + +Note that there is no recursive call in the definition of `ConsF`'s instance: +it is because we are going to use a recursion scheme that will handle the +recursion. + +We also need an instance to handle the generic `VariantF` type: + +```haskell +instance (AlgVariantF FunctorShow String xs) => FunctorShow (VariantF xs) where + functorShow = algVariantF @FunctorShow functorShow +``` + +Finally we can define a generic `eadtShow` function that uses the catamorphism +recursion scheme with the `functorShow` class method. + +```haskell +eadtShow :: + ( Functor (VariantF xs) + , FunctorShow (VariantF xs) + ) => EADT xs -> String +eadtShow = cata functorShow +``` + +We can test it: + +```haskell +intList :: List Int +intList = Cons (10 :: Int) $ Cons (20 :: Int) $ Cons (30 :: Int) Nil + +mixedList :: EADT [ConsF Int, ConsF Float, ConsF String, NilF] +mixedList = Cons @Int 10 $ Cons @Float 5.0 $ Cons "Test" Nil + +> putStrLn $ eadtShow intList +10 : 20 : 30 : Nil + +> putStrLn $ eadtShow mixedList +10 : 5.0 : "Test" : Nil +``` + + +==== Catamorphism: List (a -> a) mapping example + +Similarily to the example above, suppose that we want to implement mapping over +an EADT list. We can use the following type-class: + +```haskell +class MapEADT a xs (f :: * -> *) where + -- map the outer constructor of an EADT + mapEADT1 :: (a -> a) -> f (EADT xs) -> EADT xs +``` + +We need some instances to handle our EADT constructors: + +```haskell +instance (NilF :<: xs) => MapEADT a xs NilF where + mapEADT1 _ NilF = Nil + +instance (ConsF a :<: xs) => MapEADT a xs (ConsF a) where + mapEADT1 f (ConsF a x) = Cons (f a) x +``` + +And a additional instance to traverse the `VariantF` combinator datatype: + +```haskell +instance (AlgEADT (MapEADT a xs) xs) => MapEADT a xs (VariantF xs) where + mapEADT1 f = algVariantF @(MapEADT a xs) (mapEADT1 f) +``` + +Now we can define the `mapEADT` function by using the catamorphism combinator: + +```haskell +-- recursively map an EADT +mapEADT :: ( Functor (VariantF xs) + , MapEADT a xs (VariantF xs) + ) => (a -> a) -> EADT xs -> EADT xs +mapEADT f = cata (mapEADT1 f) +``` + +We can test it: + +```haskell +intList :: List Int +intList = Cons (10 :: Int) $ Cons (20 :: Int) $ Cons (30 :: Int) Nil + +> putStrLn $ eadtShow $ mapEADT ((+5) :: Int -> Int) intList +15 : 25 : 35 : Nil +``` + +==== Catamorphism: List (a -> b) mapping example + +Similarily, we can also support mapping with a function that changes the EADT +type as follow: + +```haskell +class TransEADT a b xs xs' (f :: * -> *) where + transEADT1 :: (a -> b) -> f (EADT xs) -> EADT xs' + +instance (NilF :<: xs') => TransEADT a b xs xs' NilF where + transEADT1 _ NilF = Nil + +instance (ConsF b :<: xs', xs ~ xs') => TransEADT a b xs xs' (ConsF a) where + transEADT1 f (ConsF a x) = Cons (f a) x + +instance TransEADT a b xs xs' (VariantF []) where + transEADT1 _ _ = undefined + +instance + ( TransEADT a b xs xs' f + , TransEADT a b xs xs' (VariantF fs) + ) => TransEADT a b xs xs' (VariantF (f : fs)) where + transEADT1 f v = case popVariantFHead v of + Right u -> transEADT1 f u + Left w -> transEADT1 f w + +transEADT :: ( Functor (VariantF xs) + , TransEADT a b xs' xs' (VariantF xs) + ) => (a -> b) -> EADT xs -> EADT xs' +transEADT f = cata (transEADT1 f) +``` + + +Note that we need to specify the resulting type as it can be anything fulfilling +the constraints: + +```haskell +> putStrLn $ eadtShow $ (transEADT (fromIntegral :: Int -> Float) intList :: List Float) +10.0 : 20.0 : 30.0 : Nil +``` + +=== Safe pattern matching with `>:>` + +Suppose we have the following `List` EADT: + +```haskell +data ConsF a l = ConsF a l deriving (Functor) +data NilF l = NilF deriving (Functor) + +eadtPattern 'ConsF "Cons" +eadtPattern 'NilF "Nil" + +type List a = EADT [ConsF a, NilF] + +-- pattern for a specific EADT: List a +pattern ConsList :: a -> List a -> List a +pattern ConsList a l = Cons a l +``` + +Using classic pattern matching on `List` constructors as we do below isn't +really typesafe because the compiler cannot detect that the pattern matching is +complete, hence we have the choice between a warning or adding a wildcard match: + +```haskell +showEADTList :: Show a => List a -> String +showEADTList = \case + ConsList a l -> show a ++ " : " ++ showEADTList l + Nil -> "Nil" + _ -> undefined -- this line avoids the warning but is unsafe + -- if we add constructors in the future +``` + + +A safe alternative is to rely on multi-continuations: we can transform any +`EADT [A,B,C]` into a function whose type is `(A -> r, B -> r, C -> r) -> +r` with the `(>:>)` operator. Then we can safely provide a function per +constructor as in a pattern-matching. + + +==== xplicit recursion example + +```haskell +import Haskus.Utils.ContFlow + +showCont' l = l >:> + ( \(ConsF a r) -> show a ++ " : " ++ showCont' r -- explicit recursion + , \NilF -> "Nil" + ) + +> showCont' intList +"10 : 20 : 30 : Nil" +``` + +==== Recursion schemes (e.g. catamorphism) + +```haskell +showCont l = l >:> + ( \(ConsF a r) -> show a ++ " : " ++ r -- no explicit recursion + , \NilF -> "Nil" + ) + +> cata showCont intList +"10 : 20 : 30 : Nil" +``` + +See recursion schemes for EADTs (@eadt-recursion-schemes). + +=== EADT Constructor removal/transformation + +Removing constructors from an EADT is equivalent to transforming every instance +of these constructors into other constructors of another EADT. + +We consider 3 cases: + +1. Fixed input EADT type; fixed list of constructors to act on + +2. Generic input EADT type; fixed list of constructors to act on + +3. Generic input EADT type; extensible list of constructors to act on + +Note in the 3 cases we need to specify the resulting EADT type as it could be +anything fulfilling the constraints. + +==== Fixed input, fixed matches + +If the type of the input EADT is fixed, we can use safe pattern-matching +(@eadt-safe-pm) as follows: + +```haskell +-- replace Even and Odd constructors with a Cons constructor +removeOddEven l = l >:> + (\(EvenF a r) -> Cons a r + ,\(OddF a r) -> Cons a r + ,\NilF -> Nil + ) + +eo :: EADT [EvenF Int, OddF Int, NilF] +eo = Even (10 :: Int) $ Odd (5 :: Int) $ Odd (7 :: Int) Nil + +> eadtShow (cata removeOddEven eo :: List Int) +"10 : 5 : 7 : Nil" +``` + +Note that `removeOddEven` only works on a specific EADT. If we want it to work on +any EADT that contains `Even` and `Odd` constructors, read the following +sections. + +==== Generic input, fixed matches + +If we want `removeEvenOdd` to work on input EADTs of any type, we can extract +the constructors that we are interested in with `splitVariantF` and lift the +left-over constructors with `liftVariantF` as follows: + +```haskell +removeOddEven x = case splitVariantF @[EvenF Int, OddF Int] x of + -- replace Even and Odd constructors with a Cons constructor + Right v -> v >:> + ( \(EvenF a l) -> Cons a l + , \(OddF a l) -> Cons a l + ) + -- do nothing to the other constructors + Left leftovers -> EADT (liftVariantF leftovers) + +eo1 :: EADT [EvenF Int, OddF Int, NilF] +eo1 = Even (10 :: Int) $ Odd (5 :: Int) $ Odd (7 :: Int) Nil + +> eadtShow (cata removeOddEven eo1 :: List Int) +"10 : 5 : 7 : Nil" + +-- additional `ConsF Int` constructor +eo2 :: EADT [ConsF Int, EvenF Int, OddF Int, NilF] +eo2 = Even (10 :: Int) $ Cons (5 :: Int) $ Odd (7 :: Int) Nil + +> eadtShow (cata removeOddEven eo2 :: List Int) +"10 : 5 : 7 : Nil" +``` + +==== Generic input, extensible matches + +If we want the `removeOddEven` pattern match to be extensible, we can use +type-classes with an overlappable instance handling the generic case (i.e. that +only transfers constructors from one EADT to another without modifying them). + +```haskell +class RemoveOddEven ys (f :: * -> *) where + removeOddEven :: f (EADT ys) -> EADT ys + +-- replace Odd and Even with Cons +instance ConsF a :<: ys => RemoveOddEven ys (OddF a) where + removeOddEven (OddF a l) = Cons a l + +instance ConsF a :<: ys => RemoveOddEven ys (EvenF a) where + removeOddEven (EvenF a l) = Cons a l + +-- handle the combinator +instance + ( AlgVariantF (RemoveOddEven ys) (EADT ys) xs + ) => RemoveOddEven ys (VariantF xs) + where + removeOddEven = algVariantF @(RemoveOddEven ys) removeOddEven + +-- handle remaining constructors +instance {-# OVERLAPPABLE #-} f :<: ys => RemoveOddEven ys f where + removeOddEven = VF -- keep the other constructors unmodified +``` + +Test: + +```haskell +eo :: EADT [EvenF Int, OddF Int, NilF] +eo = Even (10 :: Int) $ Odd (5 :: Int) $ Odd (7 :: Int) Nil + +> eadtShow (cata removeOddEven eo :: List Int) +"10 : 5 : 7 : Nil" + +-- EADT with an additional `ConsF Int` constructor +eo2 :: EADT [ConsF Int, EvenF Int, OddF Int, NilF] +eo2 = Even (10 :: Int) $ Odd (5 :: Int) $ Cons (7 :: Int) $ Odd (7 :: Int) Nil + +> eadtShow (cata removeOddEven eo2 :: List Int) +"10 : 5 : 7 : 7 : Nil" + +-- EADT with an additional `ConsF String` constructor +eo3 :: EADT [ConsF Int, EvenF Int, OddF Int, ConsF String, NilF] +eo3 = Even (10 :: Int) $ Cons "Test" $ Odd (5 :: Int) $ Cons (7 :: Int) $ Odd (7 :: Int) Nil + +> eadtShow (cata removeOddEven eo3 :: EADT [ConsF Int, ConsF String, NilF]) +"10 : \"Test\" : 5 : 7 : 7 : Nil" +``` + +We can extend `removeOddEven` to support other constructors by adding new +instances of `RemoveOddEven` for them. + +=== Splitting EADT constructors + +We can chose to handle only a subset of the constructors of an EADT by using +`splitVariantF`. + +For instance in the following example we only handle `EvenF Int` and `OddF Int` +constructors. The other ones are considered as left-overs: + +```haskell +alg x = case splitVariantF @[EvenF Int, OddF Int] x of + Right v -> v >:> + ( \(EvenF a l) -> "Even : " ++ l + , \(OddF a l) -> "Odd : " ++ l + ) + Left leftovers -> "something else" +``` + +We can test this code with: + +```haskell +eo :: EADT [EvenF Int, OddF Int, NilF] +eo = cata evenOdd intList' + +eo2 :: EADT [ConsF Int, EvenF Int, OddF Int, NilF] +eo2 = Even (10 :: Int) $ Odd (5 :: Int) $ Cons (7 :: Int) $ Odd (7 :: Int) Nil + +> cata alg eo +"Odd : Even : Odd : something else" + +> cata alg eo2 +"Even : Odd : something else" +``` + +Note that the traversal ends when it encounters an unhandled constructor. + + +=== Background on EADTs + +==== Why not Variant? + +Extensible ADT (EADT) adds support for recursive datatypes to the Variant type +(@variant). Indeed if we tried to define a recursive datatype +(e.g., a list) by using Variants, we would get the following error: + +```haskell +data Cons a l = Cons a l +data Nil = Nil + +> type L a = V [Cons a (L a), Nil] + +:19:2: error: + Cycle in type synonym declarations: + :19:2-34: type L a = V [Cons a (L a), Nil] +``` + +The issue is that there is a cyclic definition and it isn't allowed. We could +introduce ad-hoc datatypes (e.g., `newtype L a = L (V [Cons a (L a),Nil])`) to +break this cycle but this would defeat our purpose because the datatype wouldn't +be generic anymore. + +`EADT` is the datatype we use to break these cycles. By always using the same +datatype, we can provide functions that work for every EADTs. `EADT` is very +similar to the `Fix` datatype (fixed point of a functor). We use our own type to +declare our own instances. + +For example with EADTs we just have to write the following code to declare a +`List`: + +```haskell +data ConsF a l = ConsF a l deriving (Functor) +data NilF l = NilF deriving (Functor) + +type List a = EADT [ConsF a, NilF] +``` + + +==== History + +===== The expression problem (1998) + +In 1998, Philip Wadler defined the *Expression Problem* as follow: + +> The Expression Problem is a new name for an old problem. The goal is +> to define a datatype by cases, where one can add new cases to the +> datatype and new functions over the datatype, without recompiling +> existing code, and while retaining static type safety + +See: +- https://en.wikipedia.org/wiki/Expression_problem +- http://homepages.inf.ed.ac.uk/wadler/papers/expression/expression.txt + +In Haskell it is straightforward to add new functions over an ADT. Suppose +we have the following arithmetic expression ADT: + +```haskell +data Expr = Val Int | Add Expr Expr +``` + +We can independently add an evaluator function, potentially in another module: + +```haskell +eval :: Expr -> Int +eval (Val x) = x +eval (Add x y) = eval x + eval y +``` + +However if we want to add a new constructor to the ADT (say support for +multiplication), we have to modify both the ADT definition and the functions +using it: + +```haskell +data Expr = .... | Mul Expr Expr + +eval :: Expr -> Int +.... +eval (Mul x y) = eval x * eval y +``` + +What we want is to be able to add a new independent module containing both the +`Mul` constructor and the code to handle it, without modifying the other +modules defining the other constructors and the other code to handle them! + +===== Data types à la carte (2008) + +Ten years later (in 2008), Wouter Swierstra described a technique to handle this +in his well-known +#link("http://www.cs.ru.nl/~W.Swierstra/Publications/DataTypesALaCarte.pdf")[Data +types à la carte] paper. The first idea is to define data constructors +independently of the ADT and to use a type parameter to leave open the ADT they +are part of. + +```haskell +-- Independent data constructors. Parameter `e` represents the ADT they +-- will be part of. It is required even if it is not used in the right hand +-- side. +data Val e = Val Int deriving (Functor) +data Add e = Add e e deriving (Functor) +``` + +Defining a new independent constructor is easy: + +```haskell +data Mul e = Mul e e deriving (Functor) +``` + +The second idea is to use a combinator data type `:+:`: + +```haskell +data (f :+: g) e = Inl (f e) | Inr (g e) + +instance (Functor f, Functor g) => Functor (f :+: g) where ... +``` + +It is similar to `Either` except that it passes the same additional type +parameter to both `f` and `g` type constructors. It can be used to compose +independent data constructors without creating a new data type: + +```haskell +type ExprF = Val :+: Add +``` + +`ExprF` has kind `Type -> Type` and its type parameter is used as the `e` +parameter of the independent data constructors. We can set it to arbitrary types +such as `Int` to build valid values: + +```haskell +y = Inr (Add 5 8) :: ExprF Int +``` + +However the main use of this parameter should be to indicate the type of the +expression data type we want to build, say `Expr`. Hence we would like to +write something like this: + +```haskell +type Expr = ExprF Expr + + >error: + Cycle in type synonym declarations: + :12:1-22: type Expr = ExprF Expr +``` + +Oops, we can't build this cyclic (infinite) type. This leads us to the third +idea: use another data type to handle the recursive nature of the expression +type: + +```haskell +newtype Expr = Expr (ExprF Expr) +``` + +We can abstract over it to use the same data type for different expression types: + +```haskell +-- `Fix` type as defined in Data.Functor.Foldable for instance +newtype Fix f = Fix (f (Fix f)) + +type Expr = Fix ExprF +``` + +In summary, the approach uses 3 different sorts of data types: + +1. Constructor data types: `Val`, `Add`, `Mul`... + +2. Combinator data type: `:+:` + +3. Recursion handling data type: `Fix` + +By using these different data types we have untangled the construction of ADTs +(algebraic data types) and we can freely add new constructor data types and mix +them into different algebraic data types. + +Operations on these algebraic data types can be defined independently by using +type-classes and recursion schemes. + +==== EADT - Extensible ADT (2018) + +The EADT approach builds on the Swierstra's one but it replaces the combinator +data type `:+:` with the `VariantF` one based on Variant (@variant). +Similarly to the `:+:` combinator data type, `VariantF` passes its `e` +parameter to all of its "member" types and has an instance of the `Functor` +class. + +```haskell +newtype VariantF (xs :: [* -> *]) e = VariantF (Variant (ApplyAll e xs)) + +-- ApplyAll e [f,g,h] ==> [f e, g e, h e] + +instance Functor (VariantF xs) where .... +``` + +Now instead of writing `f :+: g :+: h :+: i` to combine constructor data types +to form an ADT we can write `VariantF [f,g,h,i]`. Just like using +`Variant` is more efficient -- O(1) memory usage and (de)construction -- than +using a nest of `Either`, using `VariantF` is more efficient than using a +nest of `:+:`. + +Finally an EADT is just `Fix (VariantF xs)` except that we use our own `EADT` +newtype instead of `Fix` in order to define our own additional (and non-orphan) +type-class instances. `EADT` implements `Recursive` and `CoRecursive` +type-classes from the `recursion-schemes` package, so usual `Fix` functions +should work on `EADT` too. + +```haskell +newtype EADT xs = EADT (VariantF xs) +``` + + +The next step is to define bidirectional pattern synonyms +(@eadt-pattern-synonyms) that make the manipulation of EADT values very similar +to the manipulation of usual ADTs. By using Template Haskell, these patterns can +be automatically generated. + +In summary EADTs provide a nicer interface and a better asymptotic +implementation in both memory and runtime execution than Data types à la carte. +In the future it would be better to have native support for all of this in the +language, especially to enhance compilation times by not using type families. diff --git a/doc/manual/src/stdlib/numbers.typ b/doc/manual/src/stdlib/numbers.typ new file mode 100644 index 00000000..8ee718e6 --- /dev/null +++ b/doc/manual/src/stdlib/numbers.typ @@ -0,0 +1,159 @@ +== Numbers + +=== Natural numbers + +Natural numbers are non-negative integers (0, 1, 2...). If we use a finite +numbers of bits to encode natural numbers, we can only encode a subset of the +infinite natural number set. + +#table( + columns: (auto, auto), + table.header( + [*#sym.hash bits*], [*Natural number range*] + ), + [1], [[$0$..$1$]], + [2], [[$0$..$3$]], + [3], [[$0$..$7$]], + [n], [[$0$..$2^n-1$]], +) + +`BitNat n` is the type of natural numbers encoded on `n` bits. We can define such +numbers as follow: + +```haskell +import Haskus.Format.Number + +> let x = BitNat @5 3 +> :t x +x :: BitNat 5 +``` + +Note that if we try to encode an out-of-range natural, it fails: + +```haskell +> BitNat @50 10000000000000000000000 +BitNat @50 *** Exception: `10000000000000000000000` is out of the range of values +that can be encoded by a 50-bit natural number: [0..1125899906842623] +``` + +Operations on natural numbers track the numbers of bits: + +```haskell +> BitNat @4 10 .+. BitNat @2 1 +BitNat @5 11 + +> BitNat @4 10 .*. BitNat @3 2 +BitNat @7 20 + +> BitNat @5 25 .-. BitNat @2 3 +Just (BitNat @5 22) + +> BitNat @5 2 .-. BitNat @2 3 +Nothing -- not a Natural (negative number) + +> BitNat @5 25 ./. BitNat @2 3 +Just (BitNat @5 8,BitNat @2 1) -- 25 = 8*3 + 1 +``` + +Note that we track the statically determined number of bits, not the optimal +one! For example, in `BitNat @4 10 .+. BitNat @2 1 ==> BitNat @5 11` the +result is `11` which can be encoded with a 4-bit natural but the return type +is a 5-bit natural because adding a 4-bit natural and a 2-bit natural *may* +result in a 5-bit natural: e.g. `BitNat @4 15 .+. BitNat @2 1 ==> BitNat @5 +16` and 16 can't be encoded with a 4-bit natural. + +Explicitly specifying the number of bits required to store a literal natural +value can be cumbersome so we can make GHC do it for us with the `nat` +function: + +```haskell +> nat @0 +BitNat @1 0 + +> nat @5 +BitNat @3 5 + +> nat @158748521123465897456465 +BitNat @78 158748521123465897456465 +``` + +=== Natural ranges + +Sometimes we know that the natural numbers that we manipulate are in a fixed +range: + +- An hour is in the range [1..12] +- The age of an adult is in the range [18..150] + +We can use a natural range to store those values: it ensures that the value is +in the range and it uses just the necessary bits to store (max-min+1) values. + +```haskell +> type Age = NatRange 18 150 +> natRange @25 :: Age +NatRange @18 @150 25 + +> natRange @16 :: Age +error: 16 isn't in the range [18,150] +``` + +Operations on natural ranges track range boundaries: + +```haskell +> NatRange @2 @4 3 .++. NatRange @7 @17 13 +NatRange @9 @21 16 +``` + + +// TODO: Unums +// #### Compute tables +// +// We should find ways to automatically populate look-up tables for all operations. +// +// +// ### SORN +// +// In Unums v2.0, SORN are implemented as bit sets: 1 bit per Unum. For a n bits +// Unum, the SORN is 2^n large. +// +// E.g., 8-bit unum means 256-bit SORN +// 16-bit unum means 65536-bit SORN (8 kB) +// 24-bit unum means 16777216-bit SORN (2 MB) +// 32-bit unum means 4294967296-bit SORN (512 MB) +// +// Pros: +// * manipulation is easy (bit operations) +// * manipulation time is fast and constant (no indirection, etc.) +// * precise set of Unum values +// Cons: +// * size may be too big (especially in look-up tables: 2^(3n) bits for a +// full table) +// +// We could find other SORN implementations with different trade-offs. +// +// #### Contiguous SORN +// +// We can encode contiguous SORN with two values: +// * start: the starting unum +// * count: the number of unums from start upwards +// +// Pros: +// * size is much smaller (2 * unum size), especially for look-up tables because +// connected sets remain connected under addition, subtraction, multiplication +// and division. +// * trivial logic for negate and reciprocate (i.e., operate on bounds only) +// Cons: +// * logic is a little bit more complicated because we have to mix up connected and disjoint sets +// +// #### SORN as bloom-filters +// +// In many cases, we can use Unums and SORN to reduce a search space: the computed +// solution gives us a SORN containing the solution and we may need to refine each +// Unum in the SORN to find it precisely. +// +// In these case, we could use a bloom-filter as an implementation for the SORN: it +// would potentially contain false positives but not false negative. +// +// Pros: much smaller SORN size (in bits) +// Cons: potential false positives + diff --git a/doc/manual/src/stdlib/variant.typ b/doc/manual/src/stdlib/variant.typ new file mode 100644 index 00000000..d4a10108 --- /dev/null +++ b/doc/manual/src/stdlib/variant.typ @@ -0,0 +1,1143 @@ +#import "../helpers.typ" as haskus + +== Sum types: Variant + +`V` (for `Variant`) is a sum type, i.e. a wrapper for a value which can be of +different types. For instance in the following code `x` is a variant whose value +can be an `Int`, a `Float` or a `String`: + +```haskell +import Haskus.Utils.Variant + +x :: V [Int,Float,String] +``` + +We use a type-level list of types to statically constrain the possible value +types. Compared to usual sum types (e.g. `Either Int Float`) it allows us to +have variants which can contain any number of types and to manipulate +(extend/filter/etc.) the list in a type-safe way and without requiring new data +types. + +*See also* + +- `VEither` (@veither) is a variant biased towards the first type in the list, +just like `Either a b` is biased towards the second type (`b`), allowing +instances such as `instance Functor (VEither a)` which we don't have for the `V` +variant type. + +- recursive sum types based on ``Variant`` are also supported and are called +EADT (@eadt) + + +=== Why do we need Variant? + +In the functional programming world we use algebraic data types (ADT), more +specifically #link("https://en.wikipedia.org/wiki/Tagged_union")[sum types], to +indicate that a value can be of two or more different types: + +```haskell +x,y :: Either String Int +x = Left "yo" +y = Right 10 +``` + +What if we want to support more than two types? + +*Solution 1: sum types* + +We could use different sum types with different constructors for each arity +(number of different types that the value can have). + +```haskell +data SumOf3 a b c = S3_0 a | S3_1 b | S3_2 c +data SumOf4 a b c d = S4_0 a | S4_1 b | S4_2 c | S4_3 d +``` + +But it's quite hard to work with that many different types and constructors as +we can't easily define generic functions working on different sum types without +a combinatorial explosion. + +*Solution 2: recursive ADT* + +Instead of adding new sum types we can use a nest of `Either`: + +```haskell +type SumOf3 a b c = Either a (Either b c) +type SumOf4 a b c d = Either a (Either b (Either c d)) +``` + + +Or more generically: + +```haskell +data Union (as :: [*]) where + Union :: Either (Union as) a -> Union (a : as) +``` + +This time we can define generic functions without risking a combinatorial +explosion. The drawback however is that we have changed the representation: +instead of `tag + value` where `tag` is in the range [0,arity-1] we have a +nest of `tag + (tag + (... (tag + value)))` where `tag` is in the range +[0,1]. It is both inefficient in space and in time (accessing the tag value is +in O(arity)). + +*Solution 3: variant* + +`Variant` gets the best of both approaches: it has the generic interface of +the "recursive ADT" solution and the efficient representation of the "sum types" +solution. + +```haskell +data Variant (types :: [*]) = Variant {-# UNPACK #-} !Word Any + +type role Variant representational +``` + +The efficient representation is ensured by the definition of the `Variant` +datatype: an unpacked `Word` for the tag and a "pointer" to the value. + +The phantom type list `types` contains the list of possible types for the value. +The tag value is used as an index into this list to know the effective type of the +value. + +=== How to use Variants? + +To use `Variant`: + +- add a dependency to the +#link("https://hackage.haskell.org/package/haskus-utils-variant")[haskus-utils-variant]> +package +- use the following import: `import Haskus.Utils.Variant` + +You may need to enable some language extensions: + +```haskell +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE TypeFamilies #-} +``` + +=== How to set create Variant values? + +The easiest way to create a variant value is to use the `V` pattern synonym: + +```haskell +x,y :: V [String,Int] +x = V "test" +y = V @Int 10 +``` + +For now the compiler *cannot use the variant value type list to infer the type +of the variant value*! In the previous example we have to specify the `Int` +type. Even if it's clear (for us) that it's the obvious unique possibility, it +is ambiguous for the compiler. + +```haskell +x :: V [String,Int] +x = V 10 + +-- Test.hs:12:5: error: +-- • Couldn't match type ‘Haskus.Utils.Types.List.IsMember' +-- [String, Int] c0 [String, Int]’ +-- with ‘'True’ +-- arising from a use of ‘V’ +-- The type variable ‘c0’ is ambiguous +-- • In the expression: V 10 +-- In an equation for ‘x’: x = V 10 +``` + +=== How to pattern-match on variant values? + +Matching a variant value can be done with the `V` pattern synonym too: + +```haskell +f :: V [String,Int] -> String +f = \case + V s -> "Found string: " ++ s + V (i :: Int) -> "Found int: " ++ show i + _ -> undefined +``` + +For now the compiler *cannot use the variant value type list to infer that the +pattern-match is complete*. Hence we need the wildcard match to avoid a warning. + +In section @variant-safe-pm we present another way to perform pattern +matching that doesn't require a wildcard match and that provides better type +inference. + +*Basic errors* + +If you try to set or match a value type that isn't valid, you get a compile-time +error: + +```haskell +x :: V [String,Int] +x = V @Float 10 + +-- Test.hs:14:5: error: +-- • `Float' is not a member of [String, Int] +-- • In the expression: V @Float 10 +-- In an equation for ‘x’: x = V @Float 10 +``` + +```haskell +f :: V [String,Int] -> String +f = \case + V s -> "Found string: " ++ s + V (i :: Int) -> "Found int: " ++ show i + V (i :: Float) -> "Found float: " ++ show i + _ -> undefined + +-- Test.hs:20:4: error: +-- • `Float' is not a member of [String, Int] +-- • In the pattern: V (i :: Float) +-- In a case alternative: V (i :: Float) -> "Found float: " ++ show i +``` + +==== How to pattern-match on variants safely? + +Let's suppose we have the following variant values that we want to pattern-match +on: + +```haskell +x,y,z :: V [String,Int,Float] +x = V "test" +y = V @Int 10 +z = V @Float 5.0 +``` + +*Unsafe pattern-matching* + +We can use pattern matching on the constructors as presented in section +@variant-pm: + +```haskell +printV' :: V [String,Int,Float] -> IO () +printV' = \case + V (s :: String) -> putStrLn ("Found string: " ++ s) + V (i :: Int) -> putStrLn ("Found int: " ++ show i) + V (f :: Float) -> putStrLn ("Found float: " ++ show f) + _ -> undefined + +> printV' x +Found string: test +> printV' y +Found int: 10 +> printV' z +Found float: 5.0 +``` + +However the compiler cannot detect that the pattern matching is complete, hence +we have the choice between a warning or adding a wildcard match as we have done +above. + +Now we present safer alternatives: + +*Safe pattern-matching with continuations (`>:>`)* + +Another solution is to rely on multi-continuations. Then we can provide a +function per constructor as in a pattern-matching. For instance, with +multi-continuations we can transform a variant `V [A,B,C]` into a function +whose type is `(A -> r, B -> r, C -> r) -> r`. Hence the compiler will ensure +that we provide the correct number of alternatives in the continuation tuple +(the first parameter). + +Applying a multi-continuation to a Variant is done with `>:>`: + +```haskell +import Haskus.Utils.ContFlow + +printV :: V [String,Int,Float] -> IO () +printV v = v >:> + ( \s -> putStrLn ("Found string: " ++ s) + , \i -> putStrLn ("Found int: " ++ show i) + , \f -> putStrLn ("Found float: " ++ show f) + ) +``` + +*Safe pattern-matching with unordered continuations (`>%:>`)* + +By using the `>%:>` operator instead of `>:>`, we can provide continuations in +any order as long as an alternative for each constructor is provided. + +The types must be unambiguous as the Variant constructor types can't be used to +infer the continuation types (as is done with `>:>`). Hence the type +ascriptions in the following example: + +```haskell +printU :: V [String,Int,Float] -> IO () +printU v = v >%:> + ( \f -> putStrLn ("Found float: " ++ show (f :: Float)) + , \s -> putStrLn ("Found string: " ++ s) + , \i -> putStrLn ("Found int: " ++ show (i :: Int)) + ) +``` + +=== How to get/set values by its type index? + +We can explicitly create a variant by specifying the index (starting from 0) of +the value type with `toVariantAt`: + +```haskell +x :: V [Int,String,Float] +x = toVariantAt @2 5.0 +``` + +It is especially useful if for some reason we want to have the same type more +than once in the variant value type list: + +```haskell +y :: V [Int,Int,String,Int,Float] +y = toVariantAt @1 5 +``` + +We can retrieve values by index too with `fromVariantAt`: + +```haskell +> fromVariantAt @0 x +Nothing +> fromVariantAt @1 x +Nothing +> fromVariantAt @2 x +Just 5.0 +``` + +=== How to code generic variant functions (variant-polymorphic functions)? + +In this section we show how to write generic functions that can work on +different `Variant` as long as they fulfill some constraints. + +==== How to split a variant? + +We can chose to handle only a subset of the possible value types of a Variant by +using `splitVariant`. This is very useful when your variant is open (e.g. an +exception type) and you want to perform an action for some particular +types while ignoring the others (e.g. passing the unhandled exceptions to the +caller). + +For instance in the following example we only handle `Int` and `Float` +values. The other ones are considered as left-overs: + +```haskell +printNum v = case splitVariant @[Float,Int] v of + Right v -> v >%:> + ( \f -> putStrLn ("Found float: " ++ show (f :: Float)) + , \i -> putStrLn ("Found int: " ++ show (i :: Int)) + ) + Left leftovers -> putStrLn "Not a supported number!" + +> printNum x +Not a supported number! +> printNum y +Found int: 10 +> printNum z +Found float: 5.0 +``` + +Note that the `printNum` function above is generic and can be applied to any +Variant type: + +```haskell +w,k,u :: V [String,Int,Double,Maybe Int] +w = V @Double 1.0 +k = V (Just @Int 10) +u = V @Int 17 + +> printNum w +Not a supported number! +> printNum k +Not a supported number! +> printNum u +Found int: 17 +``` + +==== `:<` and `:<<` operators + +The `c :< cs` constraint statically ensures that the type `c` is in the +`cs` type list and that we can set and match it in a variant with type `V +cs`. For example: + +```haskell +newtype Error = Error String + +showError :: (Error :< cs) => V cs -> String +showError = \case + V (Error s) -> "Found error: " ++ s + _ -> "Not an Error!" +``` + +We check that `showError` works: + +```haskell +e0,e1 :: V [String,Int,Error] +e0 = V (Error "invalid") +e1 = V @Int 10 + +> showError e0 +"Found error: invalid" + +> showError e1 +"Not an Error!" +``` + +The same generic `showError` function works with variants of other types as +well: + +```haskell +e2 :: V [Float,String,Maybe Char,Error] +e2 = V (Error "Oups!") + +e3 :: V [Error] +e3 = V (Error "Outch!") + +> showError e2 +"Found error: Oups!" + +> showError e3 +"Found error: Outch!" +``` + +Note that to shorten a list of constraints such as `(A :< xs, B :< xs, C :< xs)` +you can use the `:<<` operator: `[A,B,C] :<< xs`. + +==== `: showError e4 + +-- :45:1: error: +-- • `Error' is not a member of [String, Int] +``` + + +Nevertheless we can write a `showErrorMaybe` that works on any variant even if +it can't contain an `Error` value by using the `: V cs -> String +showErrorMaybe = \case + VMaybe (Error s) -> "Found error: " ++ s + _ -> "Not an Error!" + +> showErrorMaybe e0 +"Found error: invalid" + +> showErrorMaybe e1 +"Not an Error!" + +> showErrorMaybe e2 +"Found error: Oups!" + +> showErrorMaybe e3 +"Found error: Outch!" + +> showErrorMaybe e4 +"Not an Error!" +``` + +Obviously this example is a bit contrived because we can easily see that `e4` +can't contain an `Error`. However the same `: V cs -> V (Remove Error cs) +filterError v = case popVariantMaybe v of + Right (Error s) -> error ("Found error: " ++ s) + Left v' -> v' -- left-over variant! + + +> filterError e0 +*** Exception: Found error: invalid +CallStack (from HasCallStack): + error, called at Test.hs:61:23 in main:Main + +> filterError e1 +10 + +> :t e1 +e1 :: V [String, Int, Error] + +> :t filterError e1 +filterError e1 :: V [String, Int] + +> :t e2 +e2 :: V [Float, String, Maybe Char, Error] + +> :t filterError e2 +filterError e2 :: V [Float, [Char], Maybe Char] +``` + +Notice how an `Error` value can't be present anymore in the variant type +returned by `filterError` and how this function is generic as it supports any +variant as an input. + +Similarly we could have used the `Error <: cs` constraint and the +`popVariant` function to ensure that only variants that can contain an +`Error` value can be passed to the `filterError` function. + +=== How to convert a variant from/to a singleton value + +We can easily convert between a variant with a single value type and this value +type with `variantToValue` and `variantFromValue`: + +```haskell +intV :: V [Int] +intV = V @Int 10 + +> variantToValue intV +10 + +> :t variantToValue intV +variantToValue intV :: Int + +> :t variantFromValue "Test" +variantFromValue "Test" :: V [String] +``` + +`variantFromValue` is especially useful to avoid having to define the value +types of the variant explicitly. + +=== How to convert a variant from/to Either? + +`variantFromEither` and `variantToEither` can be used to convert between a +variant of arity 2 and the `Either` data type: + +```haskell +eith :: Either Int String +eith = Left 10 + +> :t variantFromEither eith +variantFromEither eith :: V [String, Int] + +x,y :: V [String,Int] +x = V "test" +y = V @Int 10 + +> variantToEither x +Right "test" + +> variantToEither y +Left 10 +``` + +=== How to extend the list of supported types of a variant? + +We can extend the value types of a variant by appending or prepending a list of +types with `appendVariant` and `prependVariant`: + +```haskell +x :: V [String,Int] +x = V "test" + +data A = A +data B = B + +px = prependVariant @[A,B] x +ax = appendVariant @[A,B] x + +> :t ax +ax :: V [String, Int, A, B] + +> :t px +px :: V [A, B, String, Int] +``` + +You can use the `Concat` type family to specify the type of a concatened +variant: + +```haskell +data Error0 = Error0 deriving Show +data Error1 = Error1 deriving Show + +checkErr :: + ( Int :< is + , os ~ Concat is [Error0,Error1] + , Error0 :< os + , Error1 :< os + ) => V is -> V os +checkErr = \case + V (0 :: Int) -> V Error0 + V (1 :: Int) -> V Error1 + v -> appendVariant @[Error0,Error1] v + +> checkErr (V @Int 0 :: V [Float,Int]) +V @Error0 Error0 + +> checkErr (V @Int 1 :: V [Float,Int]) +V @Error1 Error1 + +> checkErr (V @Int 2 :: V [Float,Int]) +V @Int 2 + +> checkErr (V @Float 5.0 :: V [Float,Int]) +V @Float 5.0 + +> z = checkErr (V @Float 5.0 :: V [Float,Int,String,Double]) +> :t z +z :: V [Float, Int, [Char], Double, Error0, Error1] +``` + +Appending and prepending are very cheap operations: appending just messes with +types and performs nothing at runtime; prepending only increases the tag value +at runtime by a constant number. + +These operations are used to convert a variant value into another one with a +more general variant type. See also variant lifting (@variant-lifting) which +does variant appending/prepending automatically as well as type reordering. + +=== How to extend and reorder the types of a variant? A.k.a variant lifting + +We can extend and reorder the value types of a variant with the `liftVariant` +function: + +```haskell +x :: V [String,Int] +x = V "test" + +-- adding Double and Float, and reordering +y :: V [Double,Int,Float,String] +y = liftVariant x +``` + +You can use the `LiftVariant is os` constraint to write generic code and to +ensure that the type list `is` is a subset of `os`: + +```haskell +liftX :: (LiftVariant is (Double : Float : is)) + => V is -> V (Double : Float : is) +liftX = liftVariant + +> :t liftX x +liftX x :: V [Double, Float, String, Int] + +> :t liftX (V "test" :: V [String]) +liftX (V "test" :: V [String]) :: V [Double, Float, String] +``` + +=== How to remove duplicates in a variant type list? + +If the list of types of a variant contains the same type more than once, we can +decide to only keep one of them with `nubVariant`: + +```haskell +> z = nubVariant (V "test" :: V [String,Int,Double,Float,Double,String]) +> :t z +z :: V [String, Int, Double, Float] +``` + +You can use the `Nub` type family to write generic code. + +=== How to flatten nested variants? + +If the value types of a variant are themselves variants, you can flatten them +with `flattenVariant`: + +```haskell +x :: V [String,Int] +x = V "test" + +nest :: V [ V [String,Int], V [Float,Double]] +nest = V x + +> :t flattenVariant nest +flattenVariant nest :: V [String, Int, Float, Double] +``` + +You can use the `Flattenable` type-class and the `FlattenVariant` type +family to write generic code. + +=== How to join variants of functors/monads? + +We can transform a variant of functor values (e.g., `V [m a, m b, m c]`) into +a single functor value (e.g., `m (V [a,b,c])`) with `joinVariant`: + +```haskell +fs0,fs1,fs2 :: V [ Maybe Int, Maybe String, Maybe Double] +fs0 = V @(Maybe Int) (Just 10) +fs1 = V (Just "Test") +fs2 = V @(Maybe Double) Nothing + +> joinVariant @Maybe fs0 +Just (V @Int 10) + +> joinVariant @Maybe fs1 +Just (V @[Char] "Test") + +> joinVariant @Maybe fs2 +Nothing +``` + +It also works with `IO` for example: + +```haskell +printRet :: Show a => a -> IO a +printRet a = do + print a + return a + +ms0,ms1 :: V [ IO Int, IO String, IO Double] +ms0 = V @(IO Int) (printRet 10) +ms1 = V (printRet "Test") + +> joinVariant @IO ms0 +10 +V @Int 10 + +> joinVariant @IO ms1 +"Test" +V @[Char] "Test" + +> :t joinVariant @IO ms0 +joinVariant @IO ms0 :: IO (V [Int, String, Double]) +``` + +Writing generic code requires the use of the `JoinVariant m xs` constraint and +the resulting list of value types can be obtained with the `ExtractM m xs` +type family. + +```haskell +> :t joinVariant +joinVariant :: JoinVariant m xs => V xs -> m (V (ExtractM m xs)) +``` + + +With `IO` it is possible to use the `joinVariantUnsafe` function which doesn't +require the type application and doesn't use the `JoinVariant` type-class. +However some other functor types aren't supported (e.g., `Maybe`) and using +`joinVariantUnsafe` with them makes the program crash at runtime. + +=== How to combine two variants? (i.e. variant produce) + +We can combine two variants into a single variant containing a tuple with +`productVariant`: + +```haskell +fl :: V [Float,Double] +fl = V @Float 5.0 + +d :: V [Int,Word] +d = V @Word 10 + +dfl = productVariant d fl + +> dfl +V @(Word,Float) (10,5.0) + +> :t dfl +dfl :: V [(Int, Float), (Int, Double), (Word, Float), (Word, Double)] +``` + +=== How to convert variants to tuples/HList? + +We can convert a Variant into a tuple of Maybes with `variantToTuple`: + +```haskell +w,k,u :: V [String,Int,Double,Maybe Int] +w = V @Double 1.0 +k = V (Just @Int 10) +u = V @Int 17 + +> :t variantToTuple w +variantToTuple w :: (Maybe String, Maybe Int, Maybe Double, Maybe (Maybe Int)) + +> variantToTuple w +(Nothing,Nothing,Just 1.0,Nothing) + +> variantToTuple k +(Nothing,Nothing,Nothing,Just (Just 10)) + +> variantToTuple u +(Nothing,Just 17,Nothing,Nothing) +``` + +And similarly into an HList (heterogeneous list) with `variantToHList`: + +```haskell +> variantToHList w +H[Nothing,Nothing,Just 1.0,Nothing] + +> variantToHList k +H[Nothing,Nothing,Nothing,Just (Just 10)] + +> variantToHList u +H[Nothing,Just 17,Nothing,Nothing] +``` + +=== How to map a variant type? + +We can easily apply a function `f :: A -> B` to a variant so that its value +type `A` is replaced with `B`. If the value in the variant has type `A`, +then `f` is applied to it to get the new value. Example: + +```haskell +x,y :: V [String,Int] +x = V "test" +y = V @Int 10 + +> mapVariant ((+5) :: Int -> Int) x +V @String "test" + +> mapVariant ((+5) :: Int -> Int) y +V @Int 15 +``` + +Note that the resulting variant may contain the same type more than once. To +avoid this, we can either use `nubVariant` (see @variant-nub) or directly use +`mapNubVariant`: + +```haskell +> :t mapVariant (length :: String -> Int) x +mapVariant (length :: String -> Int) x :: V [Int, Int] + +> :t mapNubVariant (length :: String -> Int) x +mapNubVariant (length :: String -> Int) x :: V [Int] + +> mapNubVariant (length :: String -> Int) x +V @Int 4 +``` + +Generic code can be written with the `MapVariant a b cs` constraint and the +`ReplaceAll` type family so that: `mapVariant :: MapVariant a b cs => (a -> +b) -> V cs -> V (ReplaceAll a b cs)` + +=== How to map a single variant type by its index? + +If we know the index of the value type we want to map, we can use +`mapVariantAt`. Example: + +```haskell +x,y :: V [String,Int] +x = V "test" +y = V @Int 10 + +> mapVariantAt @0 length x +V @Int 4 + +> mapVariantAt @0 length y +V @Int 10 + +> mapVariantAt @1 (+5) x +V @[Char] "test" + +> mapVariantAt @1 (+5) y +V @Int 15 +``` + +Note that the compiler uses the type of the element whose index is given as +first argument to infer the type of the functions `length` and `+5`, hence +we don't need type ascriptions. + +We can use `mapVariantAtM` to perform an applicative (or monadic) update. For +example: + +```haskell +add :: Int -> Int -> IO Integer +add a b = do + putStrLn "Converting the result into Integer!" + return (fromIntegral a + fromIntegral b) + +> mapVariantAtM @1 (add 5) x +V @[Char] "test" + +> mapVariantAtM @1 (add 5) y +Converting the result into Integer! +V @Integer 15 +``` + +=== How to map a the first-matching variant type? + +A variant can have the same type more than once in its value type list. +`mapVariant` (@variant-map) updates all the matching types in the list but +sometimes that's not what we want. We can use `mapVariantAt` +(@variant-map-index) if we know the index of the type we want to update. We can +also use `mapVariantFirst` as follows if we want to update only the first +matching type: + +```haskell +vv :: V [Int,Int,Int] +vv = toVariantAt @1 5 + +> r0 = mapVariant (show :: Int -> String) vv +> r1 = mapVariantFirst (show :: Int -> String) vv + +> :t r0 +r0 :: V [String,String,String] + +> :t r1 +r1 :: V [String, Int, Int] + +> r0 +V @[Char] "5" + +> r1 +V @Int 5 +``` + +We can also apply an applicative (or monadic) function with +`mapVariantFirstM`: + +```haskell +printRetShow :: Show a => a -> IO String +printRetShow a = do + print a + return (show a) + +> r2 = mapVariantFirstM (printRetShow @Int) vv +> r2 +V @Int 5 + +> :t r2 +r2 :: IO (V [String, Int, Int]) +``` + +// TODO: +// - foldMapVariantFirst[M] +// - foldMapVariant +// - alterVariant +// - traverseVariant + +=== How to use do-notation with variants? + +Note: the approach presented here uses the dreadful `RebindableSyntax` GHC extension. +We recommend that you use `VEither` instead (@veither). + +We can use `do-notation` with `Variant` as we would with other sum types +such as `Maybe` or `Either`. However, as we can't have a `Monad` instance +for `Variant`, we rely on the `RebindableSyntax` extension to mimic it. + +The leftmost type is extracted from the Variant with `>>=` (or `x <- +myVariant` with do-notation syntax). Variant types are concatenated on the +left. + +Function `foo` in the following example composes functions returning Variants +by using do-notation: + +```haskell +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE RebindableSyntax #-} + +import Haskus.Utils.Variant +import Haskus.Utils.Variant.Syntax + +import Prelude hiding (head,lookup,(>>=),(>>),return) +import qualified Prelude +import Text.Read + +foo :: String -> V [Integer, ParseError, LookupError Char, HeadError] +foo str = do + c <- head str + r <- lookup c codeMap + parse (r ++ tail str) + + where + codeMap :: [(Char, String)] + codeMap = [ ('x', "0x") + , ('d', "") + ] + + +data ParseError = ParseError deriving Show + +parse :: String -> V [Integer,ParseError] +parse s = case readMaybe s of + Just i -> V @Integer i -- we use the `V` pattern to index + Nothing -> V ParseError -- the Variant by type + +data HeadError = ListWasEmpty deriving Show + +head :: [a] -> V [a,HeadError] +head [] = toVariantAt @1 ListWasEmpty -- we can't index the Variant by +head (x:_) = toVariantAt @0 x -- type because `a` is ambiguous, + -- so we do it by index explicitly + +data LookupError k = KeyWasNotPresent k deriving Show + +lookup :: Eq k => k -> [(k,v)] -> V [v,LookupError k] +lookup k vs = case Prelude.lookup k vs of + Just v -> toVariantAt @0 v -- ditto + Nothing -> toVariantAt @1 (KeyWasNotPresent k) +``` + + +Test: + +```haskell +> foo "d10" +V @Integer 10 + +> foo "x10" +V @Integer 16 + +> foo "u10" +V @(LookupError Char) (KeyWasNotPresent 'u') + +> foo "" +V @HeadError ListWasEmpty + +> foo "d10X" +V @ParseError ParseError +``` + +=== Biased variants: VEither + +Variants have the following kind of types: `V [W,X,Y,Z]`. This is great when +all the inner types play the same role. However in some cases we want one type +to be the main one and the other ones to be secondaries. + +For instance we could have the variant whose type is `V +[Result,ErrorA,ErrorB,ErrorC]` to represent the result of a function. In this +case, the first type is the main one and it would be great to be able to define the +common type-classes (Functor, Monad, etc.) so that we have easy access to it. + +`VEither` is a Variant wrapper that does exactly this: + +```haskell +newtype VEither es a = VEither (V (a : es)) +``` + +It is isomorphic to the following type: `Either (V es) a`. The difference is +in the runtime representation: ``VEither es a`` has one less indirection than +`Either (V es) a` (it uses only one tag value). + +==== How to pattern-match on VEither values? (VRight and VLeft) + +`VEither es a` values can be created and matched on with the `VRight` and +`VLeft` patterns (just as if we had the `Either (V es) a` type). + +```haskell +>>> VRight True :: VEither [String,Int] Bool +VRight True + +>>> VLeft (V "failed" :: V [String,Int]) :: VEither [String,Int] Bool +VLeft "failed" +``` + +*Common instances* + +The main advantage of `VEither es a` over `V (a ': es)` is that we +define instances for common type-classes such as Functor, Applicative, Monad, +Foldable, etc.: + +```haskell +> let x = VRight True :: VEither [Int,Float] Bool +> fmap (\b -> if b then "Success" else "Failure") x +VRight "Success" + +> let x = VRight True :: VEither [Int,Float] Bool +> let y = VRight False :: VEither [Int,Float] Bool +> (&&) <$> x <*> y +VRight False + +> let x = VRight True :: VEither [Int,Float] Bool +> let f v = VRight (not v) :: VEither [Int,Float] Bool +> x >>= f +VRight False + +> let x = VRight True :: VEither [Int,Float] Bool +> let y = VLeft (V "failed" :: V [String,Int]) :: VEither [String,Int] Bool +> forM_ x print +True +> forM_ y print +``` + +== Multi-exceptions monad: Excepts + +Just like +#link("https://hackage.haskell.org/package/transformers-0.6.1.1/docs/Control-Monad-Trans-Except.html#g:2")[ExceptT +e m a] from the `transformers` package +wraps a `Either e a` value, we can use a `Excepts es m a` newtype to wraps a +`VEither es a` value (cf @veither) and use standard do-notation. + +Example: + +```haskell +import Haskus.Utils.Variant.Excepts + +import Prelude hiding (head,lookup) +import qualified Prelude +import Text.Read + +data ParseError = ParseError deriving Show + +parse :: String -> Excepts [ParseError] IO Integer +parse s = case readMaybe s of + Just i -> pure i + Nothing -> throwE ParseError + + +data HeadError = ListWasEmpty deriving Show + +head :: [a] -> Excepts [HeadError] IO a +head [] = throwE ListWasEmpty +head (x:_) = pure x + +data LookupError k = KeyWasNotPresent k deriving Show + +lookup :: Eq k => k -> [(k,v)] -> Excepts [LookupError k] IO v +lookup k vs = case Prelude.lookup k vs of + Just v -> pure v + Nothing -> throwE (KeyWasNotPresent k) + + + foo :: String -> Excepts [ParseError, LookupError Char, HeadError] IO Integer + -- foo :: forall es. + -- ([HeadError,ParseError,LookupError Char] :<< es + -- ) => String -> Excepts es IO Integer + foo str = do + c <- liftE $ head str + r <- liftE $ lookup c codeMap + liftE $ parse (r ++ tail str) + + where + codeMap :: [(Char, String)] + codeMap = [ ('x', "0x") + , ('d', "") + ] +``` + +Test: + +```haskell +> runE (foo "d10") +VRight 10 + +> runE (foo "x10") +VRight 16 + +> runE (foo "u10") +VLeft KeyWasNotPresent 'u' + +> runE (foo "") +VLeft ListWasEmpty + +> runE (foo "d10X") +VLeft ParseError + +> runE (foo "" `catchE` (\ListWasEmpty -> success 42) :: Excepts [ParseError,LookupError Char] IO Integer) +VRight 42 +``` + + diff --git a/doc/manual/src/system.typ b/doc/manual/src/system.typ new file mode 100644 index 00000000..19c967d5 --- /dev/null +++ b/doc/manual/src/system.typ @@ -0,0 +1,8 @@ += System Programming + +#include "system/intro.typ" +#include "system/boot.typ" +#include "system/system-management.typ" +#include "system/system-api.typ" +#include "system/graphics.typ" +#include "system/internals.typ" diff --git a/doc/manual/src/system/boot.typ b/doc/manual/src/system/boot.typ new file mode 100644 index 00000000..e5a75d7f --- /dev/null +++ b/doc/manual/src/system/boot.typ @@ -0,0 +1,11 @@ +== Booting a system + +- introduction: how does a computer boot? + - firmware: BIOS + - conventions + - architecture specific +- (UEFI system) +- Boot loader: GNU Grub, syslinux, Windows... + +- Linux kernel: a binary program + - Early userspace: @linux-initramfs diff --git a/doc/manual/src/system/graphics.typ b/doc/manual/src/system/graphics.typ new file mode 100644 index 00000000..3d10be44 --- /dev/null +++ b/doc/manual/src/system/graphics.typ @@ -0,0 +1,280 @@ +== Graphics + +=== Rendering + +==== FrameBuffer Displaying + +setControllerFB + +==== Buffer Mapping + +- Mapping buffers in user-space +- Raw drawing +- Example rectangle +- Dirty fb + +==== Configuring The Display + +- Mode settings +- automatic configuration for the connected devices in preferred modes, no cloning + +===== Setting the display mode + +The following code shows a code that tries every available mode of +a connector in sequence: each mode stays enabled for 4 seconds. To be allowed to +change the display mode, we need to create an adapted framebuffer (i.e., a +source of pixel data). You can safely ignore that for now, we will explain it in +details in Section~\ref{sec:framebuffer}. + +// codes/src/DisplayModes.hs + +- mode not supported by display device: garbage, black screen, error screen + + +==== Drawing On The Screen + +- Generic framebuffer +- full drawing example + +- Example DPMS (power-off) + +==== Multiple-Buffering And V-Blank Synchronization + +Computer screens usually have a fixed refresh rate. For instance in +Listing~\ref{lst:display_connectors_result} the first mode of the connected +display device has a (vertical) refresh rate of 60Hz. That is, 60 times per +second, the display device: + +- copies the contents of the framebuffer on the screen line-by-line: *scan-out* period +- waits for some time until the next scan-out: *v-blank* period + +===== Single Frame Buffer + +Suppose we use a single frame buffer that is displayed on the screen. If we +modify its content during the scan-out period, some artifacts may appear on the +screen. For instance if we repeatedly clear the screen, then draw a filled +rectangle and finally draw a circle on top of it, the display may either show +the cleared screen, the rectangle alone or the rectangle with the circle. The +rectangle and the circle seem to flash: this is called a *flicker* effect. + +- time to render a frame vs refresh period vs v-blank period + +- Explanation scan-out (flikering?) +- Explanation multi-buffering +- Code framebuffer swap ("page flip") +- Explanation v-blank (tearing?) +- Code synchro v-blank (event v-blank) +- Note "async page flip" flag and "page flip complete" event +- Adaptive v-sync +- Dithering (frame rate control, TN panels 6-bits per RGB) + +==== Advanced Topics + +===== Atomic Configuration + +Some drivers support an atomic configuration operation. Instead of setting a +property at a time, several properties are set at once in a transaction: if a +proprety fails to be set, the whole transaction is reverted. It ensures that the +display configuration is never left in a transition state between two +configurations.\footnote{At the time of writing, ``haskus-system`` doesn't +support this feature.} + +===== Gamma Table + +- theory, tests avec qemu non concluants + +Gamma correction consists in altering the way colors are displayed on a monitor. +For each possible value of each color channel (red, green, blue),we can define a +gamma factor. Usually there are 256 possible values per channel, but the +additional \texttt{controllerGammaTableSize} field gives the actual number of +values. Each factor is an unsigned 16-bit word. + +- Word16 or 8.8 fixed float? + +The following code shows how to retrieve and show the gamma look-up +table of a controller with ``getControllerGamma``. Similarly you can set +another gamma table with ``setControllerGamma``. + +// codes/src/DisplayGamma + +===== Sub-Pixel Rendering + +- Controller sub-pixel +- Used for fonts +- Vertical vs horizontal +- rotation property! + +=== Multi-Buffering + +==== Vertical synchronization + +Computer screens usually have a fixed refresh rate. For instance if the +display device has a (vertical) refresh rate of 60Hz, it means that 60 times per +second, the display device: + +- copies the contents of the framebuffer on the screen: scan-out period +- waits for some time until the next scan-out: `vertical blanking interval` + (v-blank interval) + +If we modify the contents of the framebuffer that is displayed on the screen +during the scan-out period, some artifacts may appear on the screen. To avoid +this, we use `vertical synchronization` (v-sync or vsync): we only modify what +is displayed during the vertical blanking interval. + +==== Multi-buffering + +If we use a single framebuffer, modifying its contents only during the vertical +blanking interval may be difficult in practice as it imposes hard deadlines to +complete the modifications. + +Instead, we can use several framebuffers: + +- the *front buffer* that is currently used for display and that is not modified +- the *back buffer(s)* that can be modified + +When a framebuffer is ready to be displayed, it becomes the "front buffer" and +the current front buffer becomes a "back buffer". The action of switching +framebuffers is called `page flipping`. + +The page flipping must occur during the v-blank interval, otherwise `screen +tearing` may appear: some part of the displayed image is taken from the first +buffer and some other part from the second one. + +If we want to start rendering a new frame without waiting for the page flipping +to complete, we can use more than one back buffer (e.g., `triple buffering`). + +==== Synchronization issues + +Rendering frames at the appropriate rate for the display may be difficult in +some cases: + +- the frame is complex and the time to render it is longer than a vsync period +- the frame rate is imposed by the source (e.g., a video encoded at 24 FPS) and + is not compatible with the display's refresh rate + +===== Adaptive vertical synchronization + +If the computer can't generate frames fast enough for some refresh rates (e.g., +in a game), it may be better to temporarily disable vertical synchronization to +reduce the latency (hence avoiding stuttering) at the cost of some visual +artefacts. This is a trade-off between image quality and sufficiently fast frame +generation speed as you can't have both. + +This is what NVIDIA names "adaptive vsync" +(http://www.geforce.com/hardware/technology/adaptive-vsync/technology>) + +===== Incompatible rates + +There are several techniques to try to deal with incompatible frame rates, such +as: + +- if a frame is displayed during several periods, take this duration into + account when rendering animated objects +- add motion blur to animated objects +- use interlaced frames + +Further reading : + +- https://blog.fishsoup.net/2011/06/22/what-to-do-if-you-cant-do-60fps/ +- https://blog.fishsoup.net/2012/11/28/avoiding-jitter-in-composited-frame-display/ +- https://en.wikipedia.org/wiki/Telecine#Frame_rate_differences +- https://en.wikipedia.org/wiki/Motion_interpolation + + +==== Programming + +===== Events + +The kernel can send events to user-space to signal the beginning of v-blank +periods and to signal the completion of page flips. + + +// TODO +// A solution +// - switch the source atomically +// - v-blank events +// Examples +// - simple rendering engine +// - link to the Clock example in appendices + +// TODO +// - time to render a frame vs refresh period vs v-blank period +// - Explanation scan-out (flikering?) +// - Explanation multi-buffering +// - Code framebuffer swap ("page flip") +// - Explanation v-blank (tearing?) +// - Code synchro v-blank (event v-blank) +// - Note "async page flip" flag and "page flip complete" event +// - Adaptive v-sync +// - Dithering (frame rate control, TN panels 6-bits per RGB) +// - mode not supported by display device: garbage, black screen, error screen + +==== Further reading + +- https://en.wikipedia.org/wiki/Multiple_buffering#Page_flipping +- https://en.wikipedia.org/wiki/Vertical_blanking_interval +- https://en.wikipedia.org/wiki/Screen_tearing + +- https://en.wikipedia.org/wiki/Multiple_buffering#Page_flipping +- https://en.wikipedia.org/wiki/Screen_tearing +- https://en.wikipedia.org/wiki/Vertical_blanking_interval +- https://en.wikipedia.org/wiki/Multiple_buffering#Triple_buffering +- https://en.wikipedia.org/wiki/Analog_television#Vertical_synchronization + +=== GUI + +Graphics User Interfaces (GUI) reflect the state of the system and let the user +interact with it. There are two things: + +- Frames: pictures that are displayed on screen + +- Interaction: given the currently displayed frame and the state of the + system (i.e. the currently displayed frame is part of the state in fact), + how to react to events (mouse click, key press, etc.) + +==== Basic game loop + +A basic game loop acts like this: + +```haskell +gameLoop :: IO () +gameLoop = do + + -- upate the state + whileM (currentTime - lastSimulationTime >= timeStep) do + -- process input events and other system events that have happened + -- during [lastSimulationTime, lastSimulationTime+timeStep] + processEvents + + updateSimulation timeStep -- update physics in constant meaningful steps + + lastSimulationTime += timeStep + + -- perform frame rendering + -- Parameter is used for interpolation (1 frame lag) or extrapolation + -- (potential glitches) of the remaining time + tmpState <- simulateUpdate (currentTime - lastSimulationTime) + render tmpState + + unlessM quitTheGame + gameLoop +``` + + +==== Modifying the state + +With MonadFlow M we track access to values from the Monad M. Basically we build +a tree of commands but if the values we read from M are the same as those in +cache, we know that the tree is exactly the same (pure function with the same +inputs). + +We build a pure tree representing the new state or we indicate if no change +occurred: then we don't have to redraw at all. + +M must be able to give a coherent view of the system at a given point in time. + +==== References + +- http://gameprogrammingpatterns.com/game-loop.html +- https://dewitters.com/dewitters-gameloop/ +- https://webcache.googleusercontent.com/search?q=cache:5cH3UfBvb2YJ:vodacek.zvb.cz/archiv/681.html&hl=en&gl=us&strip=1&vwsrc=0 diff --git a/doc/manual/src/system/images/graphics_first_pipeline.png b/doc/manual/src/system/images/graphics_first_pipeline.png new file mode 100644 index 00000000..5a71074f Binary files /dev/null and b/doc/manual/src/system/images/graphics_first_pipeline.png differ diff --git a/doc/manual/src/system/images/graphics_linux_model.svg b/doc/manual/src/system/images/graphics_linux_model.svg new file mode 100644 index 00000000..5616b186 --- /dev/null +++ b/doc/manual/src/system/images/graphics_linux_model.svg @@ -0,0 +1,962 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + Pixel colorcomponentsare sometimesin separateframe buffersdepending onpixel format + + Display + - Physical width/height- Supported modes- Sub pixel config, EDID, etc. + + + Connector + - Type + + Controller + - Mode (resolution, refresh rate, etc.) + + Plane + - Supported pixel formats- Position, rotation, scaling, size- Source Frames with offset and scaling + + + Frame + - Width/Height- Pixel format + + + FrameBuffer + - Source Buffer- Offset and pitch in the buffer- Compression, tiling... + + + Buffer + - Generic or hardware specific + + + + + + + + + + + Memory + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Clonedoutputs + + Hardwareplanecomposition + + + diff --git a/doc/manual/src/system/internals.typ b/doc/manual/src/system/internals.typ new file mode 100644 index 00000000..45ddea06 --- /dev/null +++ b/doc/manual/src/system/internals.typ @@ -0,0 +1,173 @@ +== System Internals + +=== Device management + +Internally `haskus-system` mounts a `sysfs` virtual file system through +which the Linux kernel exposes the hardware of the machine. In this file-system +each device is exposed as a sub-directory in the `/devices` directory and the +path to the device's directory uniquely identifies the device in the system. + +Directory nesting represents the device hierarchy as the system sees it. +Regular files in device directories represent device properties that can be +read and sometimes written into from user-space. Sometimes, when the tree +relationship between devices is not sufficient, relations between devices are +represented as symbolic links. + +==== File descriptor vs Handle + +Linux allows programs in user-space to have handles on kernel objects. +Suppose the kernel has an object `A` and a reference `R_A` on `A`. Instead of +directly giving `R_A` to user-space processes, the kernel maintains a +per-process array of kernel object references: `D_pid` for the process with +the `pid` identifier. To "give" `R_A` to this process, the kernel finds +an empty cell in `D_pid`, put `R_A` in it and gives the index of the cell to +the process. + +For historical reasons, the cell index is called a file descriptor and `D_pid` +a file descriptor table even if in Linux they can be used for kernel objects +that are not files (e.g., clocks, memory). User-space processes can only refer +to kernel objects through theses indirect references. Note that the file +descriptor table is specific to each process: sharing a file descriptor with +another process does not allow to share the referred kernel object. + +In `haskus-system` we use the term "handle" instead of "file descriptor" as we +find it less misleading. + +==== Device special files and /dev + +Ideally there would be a system call to get a handle on a device by providing +its unique identifier (similarly to the `getDeviceHandleByName` API provided by +`haskus-system`). Sadly it's not the case. We have to: + +1. Get the unique device triple identifier from its name + + Linux has two ways to uniquely identify devices: + + - a path in `/devices` in the `sysfs` file-system + - a triple: a major number, a minor number and a device type (`character` or + `block`). + + `haskus-system` retrieves the triple by reading different files the the + `sysfs` device directory. + +2. Create and open a device special file + + With a device triple we can create a special file (using the `mknod` system + call). + + `haskus-system` creates the device special file in a virtual file system + (`tmpfs`), then opens it and finally deletes it. + +Usual Linux distributions use a virtual file-system mounted in `/dev` and +create device special files in it. They let some applications directly access +device special files in `/dev` (e.g., X11). Access control is ensured by file +permissions (user, user groups, etc.). We don't want to do this in +`haskus-system`: we provide high-level APIs instead. + + +==== Netlink socket + +Linux dynamically adds and removes files and directories in the `sysfs` +file-system, when devices are plugged or unplugged. To signal it to user-space, +it sends kernel events in a Netlink socket. The Netlink socket is also used to +pass some other messages, for instance when the kernel wants to ask something to +the user-space. `haskus-system` handles a Netlink socket, parses received +kernel events and delivers them through a STM broadcast channel. + +In usual Linux distributions, a daemon called `udev` is responsible of +handling these kernel events. Rules can be written to react to specific events. +In particular, `udev` is responsible of creating device special file in the +`/dev` directory. The naming of theses special files is a big deal for these +distributions as applications use them directly afterwards and don't use the +other unique device identifiers (i.e., the device path in the `sysfs` +file-system). In `haskus-system`, high-level APIs are provided to avoid +direct references to device special files. + + +==== Miscellaneous + +In usual Linux distributions, `udev` (`man 7 udev`) is responsible of +handling devices. It reads `sysfs` and listens to kernel events to create and +remove device nodes in the `/dev` directory, following customizable rules. It +can also execute custom commands (`crda`, etc.) to respond to kernel requests. + + +=== Graphics + +==== "Software" rendering (i.e. on the CPU) + +For now in this manual we present a simple approach to display rendering: +basically the picture to display is generated by the CPU in host memory and then +transferred to the GPU memory (implicitly by using memory mapping). Most recent +graphic cards propose more efficient approaches: the picture to display is +generated and transformed directly by the graphic card. Instead of sending a +picture, the host sends commands or programs to be executed by the GPU. + +Currently Linux doesn't propose a unified interface to advanced graphic card +capabilities from different vendors (these are usually handled by MESA in +user-space and accessed through the OpenGL interface). `haskus-system` doesn't +provide support for them yet. + +==== Proprietary drivers + +`haskus-system` uses the Kernel Mode Setting (KMS) and the Direct +Rendering Manager (DRM) interfaces. In usual Linux distributions, some graphic +card manufacturers provide closed-source proprietary drivers that do not support +theses interfaces: they use a kernel module and user-space libraries that +communicate together by using a private protocol. The user-space libraries +provide implementations of standard high-level interfaces such as OpenGL and can +be used by rendering managers such as X.org. `haskus-system` doesn't offer a +way to use these drivers. + +==== Further reading + +The two main acronyms for Linux's display model are KMS (standing for "kernel +mode-setting") and DRM (standing for "direct rendering manager"). + +As explained in the @device-management, device drivers can support +the `ioctl` system call to handle device specific commands from the +user-space. The display interface is almost entirely based on it. Additionally, +`mmap` is used to map graphic card memory in user-space and `read` is used +to read events (V-Blank and page-flip asynchronous completion). + +In usual Linux distributions, the `libdrm` library provides an interface over +these system calls. You can learn about the low-level interface by reading the +`drm` manual (`man drm`, `man drm-kms`, etc.) or its source code at +https://cgit.freedesktop.org/mesa/drm/. + +David Herrmann has written +#link("https://dvdhrm.wordpress.com/?s=drm-mode-setting")[a good tutorial] +explaining how to use the legacy low-level display interface in the form of C +source files with detailed comments. While some details of the interface have +changed since he wrote it (e.g., the way to flip frame buffers and the atomic +interface), it is still a valuable source of information. + +The newer atomic interface is described in an article series on LWN called +"Atomic mode setting design overview" (August 2015) by Daniel Vetter: +- https://lwn.net/Articles/653071/ +- https://lwn.net/Articles/653466/ + +Wayland is the new display system for usual +Linux based distributions. It can be a great source of inspiration and of +information: +- http://wayland.freedesktop.org + +You can also read the Linux kernel code located in `drivers/gpu/drm` in the +kernel sources. + +Multi-GPU is supported by Linux. In particular: + +- Buffer sharing is supported with +#link("https://01.org/linuxgraphics/gfx-docs/drm/drm-memory-management.html\#drm-prime-support")[DRM +Prime] +- GPU switching is supported with #link("https://01.org/linuxgraphics/gfx-docs/drm/vga_switcheroo.html")[vga_switcheroo] + +https://www.elinux.org/images/4/45/Atomic_kms_driver_pinchart.pdf + +KMS/DRM history: + +- https://libv.livejournal.com/13443.html +- https://ppaalanen.blogspot.com/2014/06/from-pre-history-to-beyond-global.html +- https://lwn.net/Articles/653071 and https://lwn.net/Articles/653466/ + + diff --git a/doc/manual/src/system/intro.typ b/doc/manual/src/system/intro.typ new file mode 100644 index 00000000..19f13791 --- /dev/null +++ b/doc/manual/src/system/intro.typ @@ -0,0 +1,280 @@ +#import "../helpers.typ" as haskus + +== About haskus-system + +*haskus-system* is a framework to develop systems based on the Linux kernel. +Its main selling points are: + +- written in Haskell (systems are written in Haskell too) +- automatic building and testing (within QEMU) with the `haskus-system-build` tool +- (@haskus-system-build) +- easy to use and to modify: + #link("https://github.com/haskus/packages/haskus-system/")[all the code in a + single Git repository], documentation... +- reproducible builds: pinned versions of the Linux kernel (@system-yml) and of Haskell + dependencies (using `Cabal`) + +`haskus-system` is based *directly* and *exclusively* on the Linux kernel. +Hence, it doesn't rely on usual user-space kernel interfaces (e.g., `libdrm`, +`libinput`, `X11`, `wayland`, etc.) to communicate with the kernel. +We are free to use all the features provided by the kernel without being +constrained by the interfaces of other libraries. All the bugs are ours. + +=== About systems + +Typical computer programs don't directly deal with hardware components +(processor, video chipsets, keyboard, mouse, network chipset, storage, etc.). +Instead they rely several abstractions provided by other software. The main one +being the #link("https://en.wikipedia.org/wiki/Kernel_(operating_system)")[kernel] +which directly handles the hardware with its device-specific drivers. It +provides a common framework that all the other programs have to use to access +the hardware. + +#link("https://en.wikipedia.org/wiki/Linux_kernel")[Linux] is one of such kernels and +it is the one haskus-system uses. Typical computer programs usually don't use the interfaces +provided by the Linux kernel directly. They use abstractions built on top of +them and provided by system libraries which compose an +#link("https://en.wikipedia.org/wiki/Operating_system>")[operating system (OS)]. + +Many operating systems based on the Linux kernel use more or less the same +abstractions on top of it: these are the Unix-like +#link("https://en.wikipedia.org/wiki/Linux_distribution")[Linux distributions]. +Examples of abstractions commonly used by these distributions: `libc`, +`libinput`, `Wayland`/`X11` server, `PulseAudio`, `dbus`, etc. As they differ +only in minor ways, they can execute the same applications (`Firefox`, +`LibreOffice`, etc.). + +It is also possible to build non Unix-like operating systems on top of Linux. +These operating systems may provide totally different abstractions to the +applications. One example of such OS is +#link("https://en.wikipedia.org/wiki/Android_(operating_system)")[Android] which +mainly supports applications written in Java that use specific interfaces to +communicate with the hardware. + +`haskus-system` is a framework that provides Haskell interfaces to the Linux +kernel (hence to the hardware). It also provides higher-level interfaces built +upon them. You can use these interfaces to build custom systems (Unix-like or +not). It is also up to you to decide if your system has the concept of +"application" or not: you may design domain specific systems which provide a +single domain specific application or game. + +=== Portability + +Writing a new kernel from scratch is obviously a huge task. Pragmatically +`haskus-system` relies on an existing kernel: Linux. + +Note: the fact that `haskus-system` is based on the Linux kernel doesn't imply that +systems built with it have to provide a Unix-like interface to their +applications. This is similar to the approach followed by Google with Android: +the Linux kernel is used internally but applications have to be written in Java +and they have to use the Android interfaces. + +`haskus-system` framework and the systems using it are written with the +Haskell language. We use GHC to compile Haskell codes, hence we rely on GHC's +runtime system. This runtime system works on a bare-bones Linux kernel and +manages memory (garbage collection), user-space threading, asynchronous I/O, +etc. The runtime system has non-Haskell dependencies (libc, etc.) which are +statically linked with systems. + +==== Supported architectures + +The portability is ensured by the Linux kernel. In theory we could use our +approach on any architecture supported by the Linux kernel. In practice, we also +need to ensure that GHC supports the target architecture. + +In addition, `haskus-system` requires a thin architecture-specific layer +because Linux interface is architecture specific. Differences between +architectures include: system call numbers, some structure fields (sizes and +orders), the instruction to call into a system call and the way to pass system +call parameters (calling convention). + +The following architectures are currently supported by each level of the stack: + +- haskus-system: x86-64 +- GHC: x86, x86-64, PowerPC, and ARM +- Linux kernel: many architectures + +==== Proprietary drivers + +Some vendors do not provide open-source drivers nor documentation for their +hardware. Instead they provide pre-compiled libraries and/or kernel modules. As +they presuppose the use of some system libraries and services (`OpenGL`, +`X11`, etc.), `haskus-system` doesn't support them. + +=== Performance + +Using a high-level language such as Haskell is a trade-off between performance +and productivity. Just like using C language instead of plain assembly language +is. Moreover in both cases we expect the compilers to perform optimizations that +are not obvious or that would require complicated hard to maintain codes if they +were to be coded explicitly. + +GHC is the Haskell compiler we use. It is a mature compiler still actively +developed. It performs a lot of optimizations. In particular, it performs +inter-modules optimizations so that well-organized modular code doesn't endure +performance costs. + +Haskell codes are compiled into native code for the architecture (i.e., there is +no runtime interpretation of the code). In addition, it is possible to use LLVM +as a GHC backend to generate the native code. + +The generated native codes are linked with a runtime system provided by GHC that +manages: + +- Memory: garbage collection +- Threading: fast and cheap user-space threading +- Software transactional memory (STM): safe memory locking +- Asynchronous I/O: non-blocking I/O interacting with the threading system + +Performance-wise, this is a crucial part of the stack we use. It has been +carefully optimized and it is tunable for specific needs. It is composed of +about 40k lines of C code. + +As a last resort, it is still possible to call codes written in other languages +from Haskell through the Foreign Function Interface (FFI) or by adding a Primary +Operation (primop). ``haskus-system`` uses these mechanisms to interact with +the Linux kernel. + +*Discussion* + +It seems to us that this approach is a good trade-off. As comparison points, +most UNIX-like systems rely on unsafe interpreted shell scripts (init systems, +etc.); Google's Android (with Dalvik) used to perform runtime bytecode +interpretation and then just-in-time compilation, currently (with ART) it still +uses a garbage collector; Apple's platforms rely on a garbage collection variant +called "automatic reference counting" in Objective-C and in Swift languages +(while it might be more efficient, it requires much more care from the +programmers); JavaScript based applications and applets (unsafe language, VM, +etc.) tend to generalize even on desktop. + +=== Productivity + +Writing system code in a high-level language such as Haskell should be much more +productive than writing it in a low-level language like C. + +- High-level code is often more concise and most of the boilerplate code (e.g., + error management, logging, memory management) can be abstracted away. Fully + working code examples stay shorts and understandable. Writing system code is + much more fun as we can quickly get enjoyable results (less irrelevant details + to manage). + +- Many errors are caught during the compilation (type checking) which is + especially useful with system programming because programs are harder to debug + using standard methods (printf) and tools (gdb). + +- Code is easier to refactor thanks to type-checking, hence more maintenable. + +=== Durability and Evolution + +Our approach should be both durable and evolutive. Durable because we only use +mature technology: Linux and GHC developments both started in early 1990s and +are still very active. The only new layer in the stack is `haskus-system` +framework. All of these are open-source free software, ensuring long-term +access to the sources. + +The approach is evolutive: Haskell language is evolving in a controlled way with +GHC's extensions (and a potential future Haskell standard revision); GHC as a +compiler and a runtime system is constantly improving and support for new +architectures could be added; Linux support for new hardware and new +architectures is constantly enhanced and specific developments could be done to +add features useful for `haskus-system` (or your own system on top of it). + +`haskus-system` framework itself is highly evolutive. First it is new and +not tied to any standard. Moreover code refactoring in Haskell is much easier +than in low-level languages such as C (thanks to the strong typing), hence we +can easily enhance the framework interfaces as user code can easily be adapted. + +=== Single Code Base & Integration + +In our opinion, a big advantage of our approach is to have an integrated +framework whose source is in a single code base. It makes it much easier to +evolve at a fast pace without having to maintain interface compatibility between +its internal components. Moreover, refactoring is usually safe and relatively +easy in Haskell, so we could later split it into several parts if needed. + +#haskus.trivia[ +As a comparison point, usual Linux distributions use several system services and +core libraries, most of them in their own repository and independently +developed: `libc`, `dbus`, `udev`, `libdrm`, `libinput`, `Mesa/X11/Wayland`, +`PulseAudio`, etc. It is worth noting that the issue has been identified and +that an effort has been recently made to reduce the fragmentation and to +centralize some of them into a more integrated and coherent framework: +`systemd`. +] + +Having a single codebase written with a high-level language makes it easier to +find documentation, to understand how things work (especially the interaction +between the different components) and to make contributions. + +=== Standards + +`haskus-system` can only be used on top of the Linux kernel. It doesn't +try to follow some standards (`UNIX`, `POSIX`, `System V`, etc.) to be +portable on other kernels. In our opinion, these standards have been roadblocks +to progress in system programming because system services and applications are +usually designed to follow the least common standards to ensure portability. For +instance, useful features specific to the Linux kernel may not be used because +some BSD kernels do not support them [See also the heated debates about +`systemd` requiring Linux specific features]. With our approach, we can use +every feature of the Linux kernel and develop new ones if needed. + +It is often stated that programs should conform to the "UNIX philosophy": +each program should do only one thing and programs must be easily composable. +Despite this philosophy, `UNIX` systems often stand on feet of clay: programs are +composed with unsafe shell scripts and data exchanged between programs are +usually in weakly structured plain text format. + +In our opinion, functional programming with strong typing is much more principled +than the "UNIX philosophy": functions are by nature easily composable and their +interfaces are well-described with types. In addition, we are not limited to +plain text format and the compiler ensures that we are composing functions in +appropriate ways. + +#haskus.trivia[ +As an example, compare this with `UNIX` standard commands such as `ls` which +include many result sorting flags while the `sort` command could be used +instead: the weakly structured output of the `ls` command makes it very +inconvenient to indicate on which field to sort by (*difficult to compose*). +Moreover, the output of the `ls` command must never change, otherwise many tools +relying on it may be broken (*not evolutive*). This is because most commands do +two things: compute a result and format it to be displayed, while they should +only do the first (according to the `UNIX` philosophy). We don't have this issue +because we use type-checked data types instead of plain text. +] + +Even if `haskus-system` is in a single code base, its functions can be used in +other Haskell programs just by importing its modules. The compiler statically +checks that functions are appropriately called with valid parameters. + +#haskus.trivia[ +Compare this with the usual interface between two `UNIX` programs: parameters +from the first program have to be serialized as text and passed on the +command-line (with all the imaginable limitations on their sizes); then the +second program has to parse them as well as its standard input, to handle every +error case (missing parameter, invalid parameter, etc.), and to write the +result; finally the first program has to parse the outputs (both `stdout` and +`stderr`) of the second one and to react accordingly. For such a fundamental +concept, there is a lot of boilerplate code involved and many potential errors +lurking in it. +] + +=== Building and testing + +`haskus-system` approach allows us to quickly have a working prototype that can be tested in +an emulated environment (e.g., with `QEMU`). Especially with the +`haskus-system-build` tool that automatizes all of +the building steps (see @haskus-system-build). + +#haskus.trivia[ +As a comparison point, building a minimal usual Linux distribution from scratch +is very cumbersome as we can read in the +"#link("http://www.linuxfromscratch.org/lfs")[Linux From Scratch] " book. A lot +of different packages have to be downloaded from various places, patched, +configured, built and installed. Even if our approach is currently far from +being on par with a usual Linux distribution, we expect it to stay much more +simpler to build. +] + + + + diff --git a/doc/manual/src/system/system-api.typ b/doc/manual/src/system/system-api.typ new file mode 100644 index 00000000..aeb00380 --- /dev/null +++ b/doc/manual/src/system/system-api.typ @@ -0,0 +1,633 @@ +#import "../helpers.typ" as haskus + +== System Programming Interface + +=== How to manage devices? + +Device management is the entry-point of system programming. Programs have to +know which devices are available to communicate with the user (graphic cards, +input devices, etc.) or with other machines (network cards, etc.). + +In this guide, we present the basic concepts of device management and we show +examples with simple virtual devices provided by Linux. + +==== How to enumerate available devices? + +`haskus-system` provides an easy to use interface to list devices as detected +by the Linux kernel. To do that, use `defaultSystemInit` and +`systemDeviceManager` as in the following code: + +```haskell +import Haskus.System + +main :: IO () +main = runSys do + + sys <- defaultSystemInit + term <- defaultTerminal + let dm = systemDeviceManager sys + + inputDevs <- listDevicesWithClass dm "input" + graphicDevs <- listDevicesWithClass dm "drm" + + let + showDev dev = writeStrLn term (" - " <> show (fst dev)) + showDevs = mapM_ showDev + + writeStrLn term "Input devices:" + showDevs inputDevs + + writeStrLn term "Display devices:" + showDevs graphicDevs + + powerOff +``` + +Linux associates a class to each device. The previous code shows how to +enumerate devices of two classes: `input` and `drm` (direct rendering manager, +i.e., display devices). If you execute it in `QEMU` you should obtain results +similar to: + +``` +Input devices: + - "/virtual/input/mice" + - "/LNXSYSTM:00/LNXPWRBN:00/input/input0/event0" + - "/platform/i8042/serio0/input/input1/event1" +Display devices: + - "/pci0000:00/0000:00:01.0/drm/card0" + - "/pci0000:00/0000:00:01.0/drm/controlD64" +``` + +To be precise, we are not listing devices but event sources: a single device may +have multiple event sources; some event sources may be virtual (for instance the +`mice` input device is a virtual device that multiplexes all the mouse device +event sources and that is useful if you have more than one connected mouse +devices). + +==== How to deal with hot-pluggable devices? + +We are now accustomed to (un)plug devices into computers while they are running +and to expect them to be immediately detected and usable (i.e., without +rebooting). For instance input devices (keyboards, mice, joysticks, etc.) or +mass storages. The operating system has to signal when a new device becomes +available or unavailable. + + Linux loads some drivers asynchronously to speed up the boot. Hence devices + handled by these drivers are detected after the boot as if they had just been + plugged in. + +`haskus-system` provides an interface to receive events when the state of the +device tree changes. The following code shows how to get and print these +events: + +```haskell +import Haskus.System + +main :: IO () +main = runSys do + + term <- defaultTerminal + sys <- defaultSystemInit + let dm = systemDeviceManager sys + + -- Display kernel events + onEvent (dmEvents dm) \ev -> + writeStrLn term (show ev) + + waitForKey term + powerOff +``` + +If you execute this code in ``QEMU``, you should get something similar to: + +```haskell +-- Formatting has been enhanced for readability +KernelEvent + { kernelEventAction = ActionAdd + , kernelEventDevPath = "/devices/platform/i8042/serio1/input/input3" + , kernelEventSubSystem = "input" + , kernelEventDetails = fromList + [("EV","7") + ,("KEY","1f0000 0 0 00") + ,("MODALIAS","input:b0011v0002p0006e0000-e0,...,8,amlsfw") + ,("NAME","\"ImExPS/2Generic ExplorerMouse\"") + ,("PHYS","\"isa0060/serio1/input0\"") + ,("PRODUCT","11/2/6/0") + ,("PROP","1") + ,("REL","143") + ,("SEQNUM","850")]} +KernelEvent + { kernelEventAction = ActionAdd + , kernelEventDevPath = "/devices/platform/i8042/serio1/input/input3/mouse0" + , kernelEventSubSystem = "input" + , kernelEventDetails = fromList + [("DEVNAME","input/mouse0") + ,("MAJOR","13") + ,("MINOR","32") + ,("SEQNUM","851")]} +KernelEvent + { kernelEventAction = ActionAdd + , kernelEventDevPath = "/devices/platform/i8042/serio1/input/input3/event2" + , kernelEventSubSystem = "input" + , kernelEventDetails = fromList + [("DEVNAME","input/event2") + ,("MAJOR","13") + ,("MINOR","66") + ,("SEQNUM","852")]} +KernelEvent + { kernelEventAction = ActionChange + , kernelEventDevPath = "/devices/platform/regulatory.0" + , kernelEventSubSystem = "platform" + , kernelEventDetails = fromList + [("COUNTRY","00") + ,("MODALIAS","platform:regulatory") + ,("SEQNUM","853")]} +``` + +The three first events are due to Linux lazily loading the driver for the mouse. +The last event is Linux asking the user-space to load the wireless regulatory +information. + +==== How to make use of a device? + +To use a device, we need to get a handle (i.e., a reference) on it that we will +pass to every function applicable to it. See the code here: +https://github.com/haskus/packages/haskus-system-examples/src/device-open/Main.hs + +This code reads a 64-bit word from the `urandom` device that returns random data +and another from the `zero` device that returns bytes set to 0. Finally, we +write a string into the `null` device that discards what is written into it. +These three devices are virtual and are always available with Linux's default +configuration. + +*Device Specific Interfaces* + +In the previous code example we have used read and write methods as if the +device handle had been a normal file handle. Indeed Linux device drivers define +the operational semantics they want to give to each system call applicable to a +file handle: `read`, `write`, `fseek`, `mmap`, `close`, etc. Some +system calls may be invalid with some device handles (e.g., `write` with the +`urandom` driver). + +This gives a weak unified interface to device drivers: the system calls are the +same but the operational semantics depends on the driver. Moreover there are a +lot of corner cases, such as system call parameters or flags only valid for some +drivers. Finally, as there aren't enough "generic" system calls to cover the +whole spectrum of device features, the `ioctl` system call is used to send +device specific commands to drivers. In practice you really have to know which +device driver you're working with to ensure that you use appropriate system +calls. + +To catch up as many errors at compile time as possible, in `haskus-system` we +provide device specific interfaces that hide all this complexity. If you use +them, you minimise the risk of accidentally using an invalid system call. Some +of these interfaces are presented in the next chapters. Nevertheless you will +have to use the low-level interface presented in this chapter if you want to +write your own high-level interface to a device class not supported by +`haskus-system` or if you want to extend an existing one. + +=== How to use the logging system? + +Many high-level interfaces of the `haskus-system` use the `Sys` monad. It is +basically a wrapper for the `IO` monad that adds a logging mechanism. + +The following code prints the system log that is implicitly maintained in the +`Sys` monad on the kernel console. + +```haskell +import Haskus.System + +main :: IO () +main = runSys do + term <- defaultTerminal + writeStrLn term "Hello World!" + waitForKey term + sysLogPrint -- print system log + powerOff +``` + +Hence, the output of this program is something like: + +``` +Hello World! + +---- Log root +--*- FORK: Terminal input handler + |---- Read bytes from Handle 0 (succeeded with 1) + |---- readBytes /= 0 (success) +--*- FORK: Terminal output handler + +[ 1.818814] reboot: Power down +``` + +You can see that the log is hierarchical and that it supports thread forks: +`defaultTerminal` forks 2 threads to handle asynchronous terminal +input/output; the input thread indicates in the log that it has read 1 byte from +the terminal input (when I have pressed the `enter` key). + +Note that the log entries produced by the framework functions may change in the +future, hence the contents of the log may change and you may not get exactly the +same output if you try to execute this code. + +=== How to display graphics? + +==== Understanding the pipeline + +In this chapter, the idea is to understand the pipeline that describes where the +video displays get their pixel colors from. Configuring the pipeline is +explained in @graphics-pipeline-config. + +This pipeline directly derives from the Linux kernel API named *kernel mode +setting* (KMS) (part of the *direct rendering manager* (DRM) interface) with +some naming differences though. + +The left side of the following picture describes the relations between pipeline +entities (or objects) and the right side shows a more visual representation of +how an image is formed on a video display surface using the same entities. + +#figure( + image("images/graphics_linux_model.svg"), + caption: [ + Linux Graphics pipeline model + ] +) + +To use a video display, our task is to build such valid pipeline. There are so +many possible hardware configurations (different graphics chipsets, different +video displays, etc.) that the KMS interface is very generic. It lets us build a +pipeline quite liberally and then we can test it before enabling it for real if +it is valid. + +Controller and Plane entities of the graphics pipeline are invariant for each +graphics chipset. However Connectors are *not* invariant because some +technologies (such as +#link("https://en.wikipedia.org/wiki/DisplayPort#Multi-Stream_Transport_(MST)")[DisplayPort +Multi-Stream Transport]) +allow the use of connectors hubs which dynamically add additional Connector +entities. Frames are managed by software hence they are not invariant either. + +*Listing entities* + +As our first code example in this tutorial, we will list all the entities of all +the graphic cards we find on the system. The whole source code can be found +#link("https://github.com/haskus/packages/blob/master/haskus-system-examples/src/tutorial/TutEntitiesIDs.hs")[here]. + +We load all the graphic cards with: + +```haskell +sys <- defaultSystemInit +cards <- loadGraphicCards (systemDeviceManager sys) +``` + +Then we get entity identifiers with: + +```haskell +mids <- runE (getEntitiesIDs card) +``` + +The rest of the code deals with errors and printing the results on the terminal. + +The best way to test this code is to use `haskus-system-build` tool (cf +@haskus-system-build). + +```bash +> git clone https://github.com/haskus/packages.git +> cd packages/haskus-system-examples +> haskus-system-build test --init TutEntitiesIDs + +=================================================== + Haskus system - build config +--------------------------------------------------- +GHC version: 9.6.6 +Linux version: 6.9.9 +Syslinux version: 6.03 +Init program: TutEntitiesIDs +=================================================== +==> Building with Cabal... +[...] +==> Building ramdisk... +24986 blocs +==> Launching QEMU... +Card 0 + - Connector 31 + - Controller 35 + - Plane 33 +[ 1.026338] reboot: Power down +``` + +The tool should download, build and install the necessary dependencies and +execute the resulting system into `QEMU`. You can see that it reports one +Connector, one Controller and one Plane for the QEMU simulated graphics chipset +(the numbers are their unique identifiers). + +==== Listing displays + +To list the available video displays that are connected to the computer, we just +have to query the Connector entities and check if there is a video display +connected to them. + +The whole source code for this chapter can be found +#link("https://github.com/haskus/haskus-system/blob/master/haskus-system-examples/src/tutorial/TutDisplays.hs")[here]. +It detects the available video displays and reports information about them. + +- We retrieve information about all the entities for each card with `getEntities card` + +- Connectors (retrieved with `entitiesConnectors`) have `connectorType` and + `connectorByTypeIndex` fields which can be used to query the kind of connector (HDMI, + VGA, DVI, etc.) and the connector index for the given kind of connector. + +- Connectors also have a `connectorState` field which can be used to detect + connected display: + +```haskell +case connectorState conn of + Disconnected -> -- no connected display + ConnectionUnknown -> -- we can't know + Connected display -> -- we have a connected display! +``` + +- We get the supported modes of the display with `displayModes` field of + `display`, physical size in millimeters with `displayPhysicalWidth/Height`, the + sub-pixel layout with `displaySubPixel` (can be used to perform + #link("https://en.wikipedia.org/wiki/Subpixel_rendering")[sub-pixel rendering]) + and other properties with `displayProperties`. + +Hint: we could have used `forEachConnectedDisplay` function to do all of this +listing and filtering more simply. + +Example of run into QEMU with Linux 5.1.15: + +``` +> git clone https://github.com/haskus/packages.git +> cd packages/haskus-system-examples +> haskus-system-build test --init TutDisplays + +Probing Connector 33: Virtual-1 +Physical size: 0mm X 0 mm +Sub-pixel layout: SubPixelUnknown +Modes +1024x768 60MHz -HSync -VSync + h: width 1024 start 1048 end 1184 total 1344 skew 0 + v: width 768 start 771 end 777 total 806 scan 0 +1920x1080 60MHz -HSync -VSync + h: width 1920 start 2008 end 2052 total 2200 skew 0 + v: width 1080 start 1084 end 1089 total 1125 scan 0 +1600x1200 60MHz +HSync +VSync + h: width 1600 start 1664 end 1856 total 2160 skew 0 + v: width 1200 start 1201 end 1204 total 1250 scan 0 +[...] +Properties + var DPMS = On :: Enum [On,Standby,Suspend,Off] + var link-status = Good :: Enum [Good,Bad] + val non-desktop = False :: Bool + var CRTC_ID = 0 :: Object +``` + +*Detecting Plugging/Unplugging* + +To detect when a video display is connected or disconnected, we could +periodically list the Connectors and check their ``connectorState`` property as +we have done above. + +However a better method is to use a mechanism explained in @devices-hotplug: +when the state of a Connector changes, the kernel sends to the user-space an +event similar to the following one: + +```haskell +KernelEvent + { kernelEventAction = ActionChange + , kernelEventDevPath = "/devices/.../drm/card0" + , kernelEventSubSystem = "drm" + , kernelEventDetails = fromList + [("DEVNAME","drm/card0") + ,("MAJOR","226") + ,("MINOR","0") + ,("HOTPLUG","1") + ,("SEQNUM","1259")]} +``` + +When our system receives this event, we know it has to check the state of the +Connectors. + +Also remember that Connector entities can appear and disappear at runtime. +That's because some technologies (such as +#link("https://en.wikipedia.org/wiki/DisplayPort#Multi-Stream_Transport_(MST)")[DisplayPort +Multi-Stream Transport]) allow the use of connectors hubs which increases the +number of video displays that can be connected at the same time. + + +==== Generic buffers and frames + +The top-most elements of the graphics pipeline (@graphics-pipeline) are +Buffers. A Buffer is a memory region accessible by the graphics chipset. In this +case they are used to store pixel color components (e.g. 32-bit RGBA values). + +There are two general kinds of buffers: + +- driver specific buffers: they can be used to fully exploit the features of the + device but they use different APIs depending on the device driver. + +- generic buffers: these buffers use the same API for all devices supporting + them but they can't be used to exploit the most advanced features of the + device. + +In this chapter we present the *generic buffers* as they are simple to use and +avalable for many graphics chipsets. The source code for this chapter can be +found #link("https://github.com/haskus/haskus-system/blob/master/haskus-system-examples/src/tutorial/TutGenericFrame.hs")[here]. + +*Allocating Generic Buffers* + +To allocate a generic buffer, we can use `createGenericBuffer` function. It +takes a width and an height in pixels and the number of bits per pixels (must be +a multiple of 8). + +However we often want to create a Frame and the buffers according to the Frame +format. Hence in the code example we use ``createGenericFrame`` instead which +does all of this. Then it displays information about the allocated Frame and +Buffers. + +Example of run into QEMU with Linux 5.1.15: + +```bash +> git clone https://github.com/haskus/packages.git +> cd packages/haskus-system-examples +> haskus-system-build test --init TutCreateGenericFrame + +Frame 35 + Width: 1024 pixels + Height: 768 pixels + Pixel format: XRGB8888 (LittleEndian) + Flags: [] + FrameBuffer 0: + - Buffer handle: 1 + - Pitch: 4096 + - Offset: 0 + - Modifiers: 0 + - Buffer specific details: + - Type: generic buffer + - Width: 1024 pixels + - Height: 768 pixels + - Bits per pixels: 32 + - Flags: 0 + - Handle: 1 + - Pitch: 4096 bytes + - Size: 3145728 bytes + - Address: 0x00007efd406f5000 + +[ 0.984017] reboot: Power down +``` + +You can see that a `GenericBuffer` object contains the effective size of the +buffer (in bytes), the pitch (effective width of a line in bytes), an address +(explained in the next section), etc. + +Hint: if we want to create a generic Frame for a full screen mode, we can pass a +`Mode` to `createGenericFullScreenFrame`. Frame and Buffers dimensions (in +pixels) are then obtained from the Mode. + +*Writing into Generic Buffers* + +Generic buffers have a very useful property: they can be mapped into the process +memory. `haskus-system` automatically maps them when they are created so you +don't have to worry about doing it. + +The mapped region address is stored in a `ForeignPtr` which you can use with: +`withGenericBufferPtr` (or `withGenericFrameBufferPtr` wrapper). For example: + +```haskell +-- fill the frame with a color +withGenericFrameBufferPtr fb \ptr -> + forEachFramePixel frame \x y -> do + let off = frameBufferPixelOffset fb 4 x y -- 4 is pixel component size in bytes + pokeByteOff (castPtr ptr) (fromIntegral off) (color :: Word32) +``` + +However with generic buffers it is even easier: there is the +`forEachGenericFramePixel` wrapper that does these tricky pointer computations +for us. The code example uses it as follows: + +```haskell +-- fill the generic frame with a color +-- (0 is the FrameBuffer index) +forEachGenericFramePixel frame 0 \_x _y ptr -> + poke ptr (0x316594 :: Word32) -- write a XRGB8888 color +``` + + +==== Configuring the pipeline + +At this stage we already know enough things to +#link()[detect a connected video display] and to +#link()[allocate generic buffers and frames]. We just +need to learn how to connect entities to build +#link()[graphics pipeline] and finally display something on +the screen. + +The whole source code can be found +#link("https://github.com/haskus/haskus-system/blob/master/haskus-system-examples/src/tutorial/TutFirstPipeline.hs")[here]. + +We first need to find a primary plane and check the pixel formats it supports. +Then we need a Controller that can work with the plane (obtained with +`planePossibleControllers`). Finally we need to build the pipeline with code +similar to the following one: + +```haskell +assertLogShowErrorE "Config" <| withModeBlob card mode \modeBlobID -> + configureGraphics card Commit EnableVSync EnableFullModeset do + setConnectorSource conn ctrlID -- connector <-> controller + setPlaneTarget plane ctrlID -- controller <-> plane + setPlaneSource plane frame -- plane <-> frame + -- sizes and mode + setPlaneSize plane (frameWidth frame) (frameHeight frame) + setPlaneSourceSize plane (frameWidth frame) (frameHeight frame) + setMode ctrlID modeBlobID + -- enable the controller + enableController ctrlID True +``` + +We allocate a Mode blob on the graphic card with `withModeBlob`. Then we use +`configureGraphics` to send a batch of commands to the chipset: the commands +will either all succeed or none of them will be applied (atomicity). + +To test that a batch of commands is valid, you can pass `TestOnly` instead of +`Commit` and check for errors. + +You can allow or disallow a full mode-setting with `EnableFullModeset` and +`DisableFullModeset`. A full mode-setting is costly so avoid it if you can +afford to run in a degraded mode for some time. + +You can enable or disable vertical synchronization (VSYNC) (cf @graphics-vsync). +It is recommended to enable it to avoid tearing and because some drivers seem to +require it. + +The example code should display the following pattern on the screen: + +#figure( + image("images/graphics_first_pipeline.png"), + caption: [ + Pattern displayed by the example code + ] +) + +==== Double-bufffering and frame-switching + +In this section, we see that directly modyfing the frame that is displayed on +the screen leads to tearing/flickering and that double-buffering should be used +instead. + +Starting from the code of the previous section (@graphics-pipeline-config) , +suppose that we modify the contents of the frame continuously as we do +#link("https://github.com/haskus/haskus-system/blob/master/haskus-system-examples/src/tutorial/TutSingleFrame.hs")[here]: + +```haskell +let render frame col = do + -- fill a frame with a color + forEachGenericFramePixel frame 0 \_x _y ptr -> do + poke ptr (col :: Word32) + + renderLoop col = do + render frame col + renderLoop (col + 10) -- change the color for each frame + +sysFork "Render loop" (renderLoop 0) +``` + +If we try to execute this example, we see some flickering: sometimes the +displayed frame is not fully repaint and it has two different colors, that's why +we see some vertical line demarcating both colors. + +This is a common issue that can be solved either by: + +- only doing the rendering during the vblank period +- using two different frames and switching them during the vblank period + +The first solution only requires a single buffer but your application has to +render each frame very fast during the vblank period and before the end of the +refresh cycle. + +Using double-buffering is easier. #link("https://github.com/haskus/haskus-system/blob/master/haskus-system-examples/src/tutorial/TutFrameSwitch.hs")[Source code of the modified code example +using double-buffering]. +The change consists in allocating two frames, rendering in one when the other is +displayed and switching the frames when the rendering is over: + +```haskell +let switchFrame frame = assertLogShowErrorE "Switch frame" <| do + configureGraphics card Commit EnableVSync DisableFullModeset do + setPlaneSource plane frame + +frame1 <- createGenericFullScreenFrame card mode pixelFormat 0 +frame2 <- createGenericFullScreenFrame card mode pixelFormat 0 + +let renderLoop b col = do + let frame = if b then frame1 else frame2 + render frame col + switchFrame frame + renderLoop (not b) (col + 10) + +sysFork "Render loop" (renderLoop False 0) +``` + +When we execute this second example, the displayed frame is always fully +rendered and we don't get the flickering effect. + + diff --git a/doc/manual/src/system/system-management.typ b/doc/manual/src/system/system-management.typ new file mode 100644 index 00000000..8eb0ea20 --- /dev/null +++ b/doc/manual/src/system/system-management.typ @@ -0,0 +1,439 @@ +#import "../helpers.typ" as haskus + +== System Management + +=== How to build a system + +This section explains how to build a system: a Linux kernel and an init program. + +*Important*: the recommended approach is to use the `haskus-system-build` tool +(@haskus-system-build) which does the following steps automatically. This +section is useful to understand what the tool is doing under the hood. + +==== Building an `init` program + +Suppose we want to build the the following `HelloWorld` program +#footnote[System API is described in @system-api.]: + +```haskell +import Haskus.System + +main :: IO () +main = runSys' <| do + term <- defaultTerminal + writeStrLn term "Hello World!" + waitForKey term + powerOff +``` + +We want to build a statically linked executable to avoid the need for +distributing a system loader and some libraries (`.so`). We accomplish this with +the following `executable` section in a `.cabal` file: + +```cabal +executable HelloWorld + main-is: HelloWorld.hs + build-depends: + base, + haskus-system + default-language: Haskell2010 + ghc-options: -Wall -static -threaded + cc-options: -static + ld-options: -static -pthread + #extra-lib-dirs: /path/to/static/libs +``` + +If static versions of the `libgmp`, `libffi` and `glibc` libraries (used +by GHC's runtime system) are not available on your system, you have to compile +them and to indicate to the linker where to find them: uncomment the last line +in the previous extract of the `.cabal` file (the `extra-lib-dirs` entry) +and modify it so that the given path points to a directory containing the static +libraries. + +Then use a `cabal.project` file to declare dependencies on the haskus packages +you need. For example, in the `haskus-system-examples` directory, we use the +following `cabal.project` to depend on development versions of some packages: + +```yaml +packages: + . + ../haskus-system + ../haskus-utils-variant + ../haskus-utils-types + ../haskus-utils-data + ../haskus-utils-compat + ../haskus-utils + ../haskus-binary + ../haskus-ui + +program-options + ghc-options: -fhide-source-paths +``` + +Then use `cabal build HelloWorld` to compile the program. + +Then use `cabal list-bin HelloWord` to localize the generated binary file that we will +use as `init` program: + +```bash +> cabal list-bin HelloWorld +/home/hsyl20/projects/haskus/packages/haskus-system-examples/dist-newstyle/build/x86_64-linux/ghc-9.6.6/haskus-system-examples-0.1.0.0/x/HelloWorld/build/HelloWorld/HelloWorld +``` + +==== Building the Linux kernel + +The Linux kernel is required to execute systems using `haskus-system`. Leaving +aside modules and firmwares, a compiled Linux kernel is a single binary file. + +To build Linux, you first need to download it from https://kernel.org and to unpack +it: + +```bash +> wget https://www.kernel.org/pub/linux/kernel/v4.x/linux-4.9.8.tar.xz +> tar xf linux-4.9.8.tar.xz +``` + +Then you need to configure it. We recommend at least the following: + +```bash +> cd linux-4.9.8 + +# default configuration for the X86-64 target +> make x86_64_defconfig + +# enable some DRM (graphics) drivers +> ./scripts/config -e CONFIG_DRM_BOCHS +> ./scripts/config -e CONFIG_DRM_RADEON +> ./scripts/config -e CONFIG_DRM_NOUVEAU +> ./scripts/config -e CONFIG_DRM_VIRTIO_GPU + +# fixup configuration (use default values) +> make olddefconfig +``` + +If you know what you are doing, you can configure it further with: + +```bash +> make xconfig +``` + +Finally, build the kernel with: + +```bash +> make -j8 +``` + +Copy the resulting kernel binary that you can use with QEMU for instance: + +```bash +> cp arch/x86/boot/bzImage linux-4.9.8.bin +``` + +You can also copy built modules and firmwares with: + +```bash +> make modules_install INSTALL_MOD_PATH=/path/where/to/copy/modules +> make firmware_install INSTALL_FW_PATH=/path/where/to/copy/firmwares +``` + +==== Building the `initramfs` archive + +After its initialization, the Linux kernel creates a virtual file system in +memory (`initramfs`) and runs the `/init` program from it (or another program +specified by a kernel flag). We need to prepare an archive file containing the +files we want loaded in this virtual file system. + +To do that, put the files you want (at least the `init` program built in +@build-init-program) into a directory `/path/to/my/system`. +Then +execute: + +```bash +(cd /path/to/my/system ; find . | cpio -o -H newc | gzip) > myimage.img +``` + +You need to have the `cpio` and `gzip` programs installed. It builds a +ramdisk file named `myimage.img` in the current directory. + +Note that `haskus-system-build` should soon use its own implementation of +`cpio`. See https://github.com/haskus/packages/issues/59 + +=== How to test a system with QEMU + +You can test a system with QEMU. You only need: +- a linux kernel binary (see @build-linux-kernel): e.g. `linux.bin` +- an initramfs archive (see @build-initramfs), e.g. `myimage.img` + +If the filepath of the `init` program to run in the `initramfs` is `/my/system`, +then you can test it with QEMU as follows: + +```bash +qemu-system-x86_64 + -kernel linux.bin + -initrd myimage.img + -append "rdinit=/my/system" +``` + +We recommend the following options for `QEMU`: + +```bash +# make QEMU faster by using KVM (if supported by your host system) +-enable-kvm + +# use newer simulated hardware +-machine q35 + +# Increase the amount of memory available for the guest +-m 8G + +# redirect the guest Linux console on the host terminal +-serial stdio +-append "console=ttyS0" + +# make the guest Linux output more quiet +-append "quiet" +``` + +=== How to distribute a system + +To distribute your systems, create a temporary directory (say `/my/disk`) +containing: + +- your system (in an initramfs archive, cf @build-initramfs) +- the Linux kernel binary (cf @build-linux-kernel) +- the boot-loader files (including its configuration) + +A boot-loader is needed as it loads Linux and the initramfs archive containing +your system. We use Syslinux boot-loader but you can use others such as GRUB. +Note that you don't need a boot-loader when you test your system with QEMU +because QEMU acts as a boot-loader itself. + +To distribute your systems, you can install the boot-loader on a device (e.g., +USB stick) and copy the files in the `/my/disk` directory on it. Or you can +also create a `.iso` image to burn on a CD-ROM (or to distribute online). + + +==== Downloading Syslinux + +You first need to download and unpack the Syslinux boot-loader: + +```bash +> wget http://www.kernel.org/pub/linux/utils/boot/syslinux/syslinux-6.03.tar.xz +> tar xf syslinux-6.03.tar.xz +``` + +==== Creating the disk directory + +You need to execute the following steps to create your disk directory: + +Create some directories: + +```bash +> mkdir -p /my/disk/boot/syslinux +``` + +Copy Syslinux: + +```bash +> find syslinux-6.03/bios *.c32 -exec cp {} /my/disk/boot/syslinux ; +> cp syslinux-6.03/bios/core/isolinux.bin /my/disk/boot/syslinux/ +``` + +Copy the Linux kernel: + +```bash +> cp linux-4.9.8.bin /my/disk/boot/ +``` + +Copy the system ramdisk: + +```bash +> cp myimage.img /my/disk/boot/ +``` + +Finally, we need to configure the boot-loader by creating a file +`/my/disk/boot/syslinux/syslinux.cfg` containing: + +```ini +DEFAULT main +PROMPT 0 +TIMEOUT 50 +UI vesamenu.c32 + +LABEL main +MENU LABEL MyOS +LINUX /boot/linux-4.9.8.bin +INITRD /boot/myimage.img +APPEND rdinit="/my/system" +``` + +Replace `/my/system` with the path of your system in the ``myimage.img`` +ramdisk. + + +==== Creating a bootable device + +To create a bootable device (e.g., bootable USB stick), you have to know its +device path (e.g., `/dev/XXX`) and the partition that will contain the boot +files (e.g., `/dev/XXX_N`). + +You can use `fdisk` and `mkfs.ext3` to create an appropriate partition. + +You have to install Syslinux MBR: + +```bash +> sudo dd bs=440 if=syslinux-6.03/bios/mbr/mbr.bin of=/dev/XXX +``` + +Then you have to copy the contents of the disk directory on the partition and +configure it to be bootable: + +```bash +> sudo mount /dev/XXX_N /mnt/SOMEWHERE +> sudo cp -rf /my/disk/* /mnt/SOMEWHERE +> sudo syslinux-6.03/bios/extlinux/extlinux --install /mnt/SOMEWHERE/boot/syslinux +> sudo umount /mnt/SOMEWHERE +``` + +Now your device should be bootable with your system! + + +==== Creating a bootable ISO + +To create a bootable CD-ROM, you first need to create a `.iso` disk image with +the `xorriso` utility: + +```bash +xorriso -as mkisofs + -R -J # use Rock-Ridge/Joliet extensions + -o mydisk.iso # output ISO file + -c boot/syslinux/boot.cat # create boot catalog + -b boot/syslinux/isolinux.bin # bootable binary file + -no-emul-boot # does not use legacy floppy emulation + -boot-info-table # write additional Boot Info Table (required by SysLinux) + -boot-load-size 4 + -isohybrid-mbr syslinux-6.03/bios/mbr/isohdpfx_c.bin # hybrid ISO + /my/disk +``` + +It should create a `mydisk.iso` file that you can burn on a CD or distribute +online. + + +=== The haskus-system-build tool + +The `haskus-system-build` tool helps automating the steps required to build +(@build-system), to test (@test-system), and to distribute systems +(@distribute-system). + +It requires the following externals programs (or commands): +- git +- tar, lzip, gzip, cpio +- make, gcc, binutils... +- cabal-install +- dd, (u)mount, cp +- qemu +- xorriso + +==== Command-line interface + +This is the reference for the `haskus-system-build` program command-line +interface. + +Commands: + +- `init`: create a new project from a template + + - `--template` or `-t` (optional): template name + +- `build`: build the project and its dependencies (Linux) + +- `test`: launch the project into QEMU + + - `--init` (optional): specify an init program. It overrides `ramdisk.init` + in `system.yaml` (cf @system-yml) + +- `make-disk`: create a directory containing the whole system + + - `--output` or `-o` (mandatory): output directory + +- `make-iso`: create an ISO image of the system + +- `test-iso`: test the ISO image with QEMU + +- `make-device`: install the system on a device + + - `--device` or `-d` (mandatory): device path (e.g., `/dev/sdd`). For now, + the first partition is used as a boot partition. + +Note that the tool also builds `libgmp` as it is required to statically link +programs produced by GHC. Some distributions (e.g., Archlinux) only provide +`libgmp.so` and not `libgmp.a`. + +==== `system.yaml` syntax + + +This is the reference for `system.yaml` files used by `haskus-system-build` +tool (@haskus-system-build). + +*Linux kernel* + +- `linux.source`: how to retrieve the Linux kernel + + - `tarball` (default) + - `git` (not yet implemented) + +- `linux.version`: which Linux version to use + + - requires `linux.version=tarball` + +- `linux.options`: + + - `enable`: list of Linux configuration options to enable + - `disable`: list of Linux configuration options to disable + - `module`: list of Linux configuration options to build as module + +- `linux.make-args`: string of arguments passed to `make` + +*Ramdisk* + +- `ramdisk.init`: name of the program to use as init program + + +*QEMU* + +- `qemu.profile`: option profile to use + + - `default` (default): enable some recommended options + - `vanilla`: only set required options (-kernel, etc.) + +- `qemu.options`: string of additional arguments to pass to QEMU + +- `qemu.kernel-args`: string of additional arguments to pass to the Kernel + +*Example* + +```yaml +linux: + source: tarball + version: 4.11.3 + options: + enable: + - CONFIG_DRM_BOCHS + - CONFIG_DRM_VIRTIO + disable: + - CONFIG_DRM_RADEON + module: + - CONFIG_DRM_NOUVEAU + make-args: "-j8" + +ramdisk: + init: my-system + +qemu: + profile: vanilla + options: "-enable-kvm" + kernel-args: "quiet" +``` + + diff --git a/doc/manual/typst.sh b/doc/manual/typst.sh new file mode 100755 index 00000000..94106ac6 --- /dev/null +++ b/doc/manual/typst.sh @@ -0,0 +1,2 @@ +#!/bin/sh +typst $@ --font-path fonts/