More work on draft
This commit is contained in:
parent
2afc2b9d55
commit
18a4eac1f1
1 changed files with 175 additions and 11 deletions
|
|
@ -7,13 +7,14 @@ import Data.List
|
|||
import Data.List.Elem
|
||||
import Data.List.Quantifiers
|
||||
|
||||
import System
|
||||
|
||||
import DependentNuggets.FreshLists
|
||||
```
|
||||
|
||||
Sometimes, especially when dealing with business logic, we have to deal with data that comes in from the real world, or elsewhere, naturally very messily typed, leading to nasty type signatures and messes of macros or code generation to build data structures from a schema. Row polymorphism can help us by abstracting over the fields contained in a record type in the type signature, letting us define records based on data, concatenate records together, and define functions that are generic across any record containing the required fields, all without macros.
|
||||
|
||||
This article is inspired by my work on implementing the _Brown Benchmark for Table Types_(B2T2)[^1] for my _Structures_[^2] library, an update for which will be released soon, providing a much more comprehensive collection of types for row-polymorphic programming.
|
||||
This article is inspired by my work on implementing the _Brown Benchmark for Table Types_[^1] for my _Structures_[^2] library, an update for which will be released soon, providing a much more comprehensive collection of types for row-polymorphic programming.
|
||||
|
||||
|
||||
## What is Row Polymorphism
|
||||
|
|
@ -75,9 +76,11 @@ Imagine you are helping your friend move and they need to figure out what furnit
|
|||
|
||||
| room → String | length → Double | width → Double |
|
||||
|---------------|-----------------|----------------|
|
||||
| Bedroom | 3.00 | 6.00 |
|
||||
| Kitchen | 2.50 | 2.00 |
|
||||
| Bathroom | 1.50 | 1.00 |
|
||||
| Bedroom | 3.65 | 3.35 |
|
||||
| Living Room | 4.87 | 3.35 |
|
||||
| Dining Room | 2.44 | 2.44 |
|
||||
| Kitchen | 3.35 | 2.44 |
|
||||
| Bathroom | 3.65 | 2.44 |
|
||||
|
||||
</div>
|
||||
|
||||
|
|
@ -93,9 +96,12 @@ Imagine you are helping your friend move and they need to figure out what furnit
|
|||
|
||||
| item → String | length → Double | width → Double | height → Double |
|
||||
|---------------|-----------------|----------------|-----------------|
|
||||
| Dresser | 1.00 | 0.25 | 0.80 |
|
||||
| Chair | 0.50 | 0.50 | 1.00 |
|
||||
| Nightstand | 0.75 | 0.50 | 0.50 |
|
||||
| Dresser | 1.00 | 0.60 | 0.76 |
|
||||
| Bed | 2.00 | 1.50 | 0.50 |
|
||||
| Nightstand | 0.60 | 0.48 | 0.75 |
|
||||
| Dinner Table | 1.80 | 0.90 | 0.80 |
|
||||
| TV Stand | 1.93 | 0.42 | 0.90 |
|
||||
| Coffee Table | 1.81 | 0.81 | 0.46 |
|
||||
|
||||
</div>
|
||||
|
||||
|
|
@ -132,6 +138,11 @@ record Header where
|
|||
constructor MkHeader
|
||||
label: String
|
||||
type: Type
|
||||
|
||||
export infixr 8 :>
|
||||
public export
|
||||
(:>) : String -> Type -> Header
|
||||
(:>) str x = MkHeader str x
|
||||
```
|
||||
|
||||
The schema itself is really simple, just an alias for a list of headers:
|
||||
|
|
@ -151,7 +162,8 @@ We will also need a way to compute the column types from our schema, turning a l
|
|||
```idris
|
||||
public export
|
||||
ColumnTypes : Schema -> List Type
|
||||
ColumnTypes xs = map type xs
|
||||
ColumnTypes [] = []
|
||||
ColumnTypes (h :: hs) = h.type :: ColumnTypes hs
|
||||
```
|
||||
|
||||
### Making a row
|
||||
|
|
@ -164,7 +176,7 @@ A row is a list of the same length as the schema where every list element has a
|
|||
```idris
|
||||
public export
|
||||
Row : Schema -> Type
|
||||
Row xs = HList (ColumnTypes xs)
|
||||
Row hs = HList (ColumnTypes hs)
|
||||
```
|
||||
|
||||
We will also want a way of indexing the values in a row by their columns, instead of by their positions. We only want this function to be callable when the row actually _has_ that column, so we also require an inclusion proof, as an auto-implicit so the compiler can generate it for us when possible:
|
||||
|
|
@ -182,11 +194,163 @@ namespace RowIndex
|
|||
|
||||
### Making a table
|
||||
|
||||
The table itself is pretty simple, its just a list of rows:
|
||||
|
||||
```idris
|
||||
public export
|
||||
Table : Schema -> Type
|
||||
Table hs = List (Row hs)
|
||||
```
|
||||
|
||||
## Using our tables
|
||||
|
||||
## Row polymorphic functions
|
||||
Now that we have a way to describe the type signature of a table, let's go ahead and translate our previous table examples into code:
|
||||
|
||||
### Revisiting our furniture example
|
||||
```idris
|
||||
Rooms : Schema
|
||||
Rooms = ["room" :> String, "length" :> Double, "width" :> Double]
|
||||
|
||||
rooms : Table Rooms
|
||||
rooms =
|
||||
[ ["Bedroom", 3.65, 3.35]
|
||||
, ["Living Room", 4.87, 3.35]
|
||||
, ["Dining Room", 2.44, 2.44]
|
||||
, ["Kitchen", 3.35, 2.44]
|
||||
, ["Bathroom", 3.65, 2.44]
|
||||
]
|
||||
```
|
||||
|
||||
```idris
|
||||
Furniture : Schema
|
||||
Furniture = ["item" :> String, "length" :> Double, "width" :> Double, "height" :> Double]
|
||||
|
||||
furniture : Table Furniture
|
||||
furniture =
|
||||
[ ["Dresser", 1.00, 0.60, 0.76]
|
||||
, ["Bed", 2.00, 1.50, 0.50]
|
||||
, ["Nightstand", 0.60, 0.48, 0.75]
|
||||
, ["Dinner Table", 1.80, 0.90, 0.80]
|
||||
, ["TV Stand", 1.93, 0.42, 0.90]
|
||||
, ["Coffee Table", 1.81, 0.81, 0.46]
|
||||
]
|
||||
```
|
||||
|
||||
### A simple row polymorphic function
|
||||
|
||||
With our tables defined, it's time to revisit our `area` function. The schema will be an implicit variable in the type signature, and we'll constrain it such that both the length and width fields are elements of the schema. These constraints allow us to simply call the `index` function with the given fields on the provided row:
|
||||
|
||||
> [!TIP]
|
||||
> In a type signature, `x =>` is equivalent to `{auto _ : x} ->`
|
||||
|
||||
```idris
|
||||
area : {hs : Schema} -> "length" :> Double `Elem` hs => "width" :> Double `Elem` hs =>
|
||||
Row hs -> Double
|
||||
area x =
|
||||
let length = ("length" :> Double) `index` x
|
||||
width = ("width" :> Double) `index` x
|
||||
in length * width
|
||||
```
|
||||
|
||||
Without any further work, we can now call this function on both our room and furniture tables and it works as expected:
|
||||
|
||||
> [!NOTE]
|
||||
> In this specific context, we do have to explicitly provide the schema to the `area` function to disambiguate, but this can be worked around and should be considered more of an artifact of the limited implementation in this blog post then an intrinsic ergonomics concern.
|
||||
|
||||
```idris hide
|
||||
-- @@test map area rooms
|
||||
mapAreaRooms : IO Bool
|
||||
mapAreaRooms = do
|
||||
pure $
|
||||
```
|
||||
|
||||
<div class="unit-test">
|
||||
```idris
|
||||
map (area {hs = Rooms}) rooms == [12.2275, 16.314500000000002, 5.9536, 8.174, 8.905999999999999]
|
||||
```
|
||||
</div>
|
||||
|
||||
```idris hide
|
||||
-- @@test map area furniture
|
||||
mapAreaFurniture : IO Bool
|
||||
mapAreaFurniture = do
|
||||
pure $
|
||||
```
|
||||
|
||||
<div class="unit-test">
|
||||
```idris
|
||||
map (area {hs = Furniture}) furniture == [0.6, 3.0, 0.288, 1.62, 0.8106, 1.4661000000000002]
|
||||
```
|
||||
</div>
|
||||
|
||||
### Building a new column
|
||||
|
||||
Just being able to access the fields in a row polymorphic way is pretty neat, but its also not really that impressive. We have much more interesting capabilities at our disposal, like adding new fields. We can take a function that consumes a row and produces a new value, along with a name for the new value, and use that to add a new column to each row in the table:
|
||||
|
||||
```idris
|
||||
buildColumn : {hs : Schema}
|
||||
-> (f : Row hs -> t) -> (name : String) -> Table hs -> Table (hs ++ [name :> t])
|
||||
buildColumn f name table = map buildColumnRow table
|
||||
where
|
||||
addToEnd : {name' : String} -> {hs' : Schema}
|
||||
-> t -> Row hs' -> Row (hs' ++ [name' :> t])
|
||||
addToEnd {hs' = []} x [] = [x]
|
||||
addToEnd {hs' = (y :: ys)} x (x' :: xs) = x' :: addToEnd x xs
|
||||
buildColumnRow : {name' : String} -> Row hs -> Row (hs ++ [name' :> t])
|
||||
buildColumnRow row = addToEnd (f row) row
|
||||
```
|
||||
|
||||
With this new under our belt, we can make new tables derived from our previous ones, such as adding an area column to our previous two tables:
|
||||
|
||||
```idris
|
||||
roomsWithArea : Table (Rooms ++ ["footprint" :> Double])
|
||||
roomsWithArea = buildColumn {hs = Rooms} (area {hs = Rooms}) "footprint" rooms
|
||||
```
|
||||
|
||||
```idris hide
|
||||
-- @@test roomsWithArea
|
||||
roomsWithAreaTest : IO Bool
|
||||
roomsWithAreaTest = do
|
||||
pure $
|
||||
```
|
||||
|
||||
<div class="unit-test">
|
||||
```idris
|
||||
roomsWithArea ==
|
||||
[ ["Bedroom", 3.65, 3.35, 12.2275]
|
||||
, ["Living Room", 4.87, 3.35, 16.314500000000002]
|
||||
, ["Dining Room", 2.44, 2.44, 5.9536]
|
||||
, ["Kitchen", 3.35, 2.44, 8.174]
|
||||
, ["Bathroom", 3.65, 2.44, 8.905999999999999]
|
||||
]
|
||||
```
|
||||
</div>
|
||||
|
||||
```idris
|
||||
furnitureWithArea : Table (Furniture ++ ["footprint" :> Double])
|
||||
furnitureWithArea = buildColumn {hs = Furniture} (area {hs = Furniture}) "footprint" furniture
|
||||
```
|
||||
|
||||
```idris hide
|
||||
-- @@test furnitureWithArea
|
||||
furnitureWithAreaTest : IO Bool
|
||||
furnitureWithAreaTest = do
|
||||
pure $
|
||||
```
|
||||
|
||||
<div class="unit-test">
|
||||
```idris
|
||||
furnitureWithArea ==
|
||||
[ ["Dresser", 1.0, 0.6, 0.76, 0.6]
|
||||
, ["Bed", 2.0, 1.5, 0.5, 3.0]
|
||||
, ["Nightstand", 0.6, 0.48, 0.75, 0.288]
|
||||
, ["Dinner Table", 1.8, 0.9, 0.8, 1.62]
|
||||
, ["TV Stand", 1.93, 0.42, 0.9, 0.8106]
|
||||
, ["Coffee Table", 1.81, 0.81, 0.46, 1.4661000000000002]
|
||||
]
|
||||
```
|
||||
</div>
|
||||
|
||||
### Select
|
||||
|
||||
### Implementing Regular Interfaces for Row Types
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue