Extensible records for Idris, using Haskell's HList as inspiration for its design and API.
To be able to run this project on your local machine you need to have Idris
installed. Follow these instructions: https://github.com/idris-lang/Idris-dev/wiki/Installation-Instructions
Afterwards, clone the repository and you can start working on the project.
If you want to load the project into the Idris REPL do the following:
idris src/extensible_records.idr
If you want to load the samples into the RELP then do:
idris src/samples.idr
To create records you can use the .*.
operator, ending in a call to the empty record emptyRec
, like so:
r1 : Record [("surname", String), ("age", Int)]
r1 = ("surname" .=. "Bond") .*.
("age" .=. 30) .*.
emptyRec
To extend a record with new fields, call the .*.
operator again:
rExtended : Record [("name", String), ("surname", String), ("age", Int)]
rExtended = ("name" .=. "James") .*. r1
Beyond record extension, you can manipulate extensible records in many other ways using other operators. Here examples of some operators:
r2 : Record [("surname", String), ("name", String)]
r2 = ("surname" .=. "Bond") .*.
("name" .=. "James") .*.
emptyRec
r3 : Record [("name", String), ("code", String)]
r3 = ("name" .=. "James") .*.
("code" .=. "007") .*.
emptyRec
-- Lookup
r1 .!. "surname"
-- Append
rAppend : Record [("surname", String), ("age", Int), ("name", String), ("code", String)]
rAppend = r1 .++. r3
-- Update
rUpdate : Record [("surname", String), ("age", Int)]
rUpdate = updR "surname" r1 "Dean"
-- Delete
rDelete : Record [("age", Int)]
rDelete = "surname" .//. r1
You can find more examples and ways to use such operators in the samples.idr
file.
We use SemVer for versioning. For the versions available, see the tags on this repository.
This project is licensed under the MIT License - see the LICENSE file for details
Big thank you to my professors Alberto Pardo and Marcos Viera from Universidad de la Republica for helping and guiding me in developing this library for my bacherlor thesis. Also thank you to the wonderful Idris community who provided helpful advice via IRC.