iddys

it's a little tedious managing multiple libraries you are working on locally with pack, so this is more or less all vaguely general purpose idris code dysfun has written, along with some stuff that isn't generally useful.

Things may (will!) be incomplete and subject to change.

Contents

Bits and bytes

Most of these are in support of the patricia trie

• Bits - masked bit extraction and deposit
• Bits.Digit - some obvious missing stuff from Data.Binary.Digit
• Bits.Pop - proof of popcount
• Bitset - a fixed size set of bits indexed by an enumerable tag type
• Endian - fixed length big-endian bitstrings
• Endian.Asc - proof that a vector of bitstrings are ordered
• Endian.Prefix - proofs that a bitstring begins with some bitstring
• Endian.Nth - proof that the nth item in the vector is some bit
• Endian.Match - matching prefixes of bitstrings
• Endian.LT - relative comparison of bitstrings

Nat utilities

• Data.Finite - Fin, via Nat + LT
• Data.Nat.More - missing Nat stuff

List utilities

• Data.List.Paired - a proof that two lists are the same length
• Data.List.Quantifiers.Fold - asserts that a proof holds for all elements relative to all successive elements.
• Data.List.Set - asserts that a vector contains no duplicates by DecEq (slowly!)
• Data.List.Subseq - a subsequence relation maintaining order and supporting gaps
• Data.List.Subseq.Elem - tools for working with subsequences and Elem

Vector utilities

• Data.Vect.ElemAt - like Data.Vect.AtIndex but indexed by Nat instead of Fin
• Data.Vect.Equals - proof that a vector's contents are all the same
• Data.Vect.Insert - a vector insert as a data structure
• Data.Vect.Quantifiers.Fold - asserts that a proof holds for all elements relative to all successive elements.
• Data.Vect.Quantifiers.Pow - asserts that a proof holds for all elements relative to all other elements.
• Data.Vect.Set - a vector with no duplicates
• Data.Vect.More - missing vector stuff

List utilities

• Data.List.Paired - a proof that two lists are the same length
• Data.List.Quantifiers.Fold - asserts that a proof holds for all elements relative to all successive elements.
• Data.List.Set - asserts that a vector contains no duplicates by DecEq (slowly!)
• Data.List.Subseq - a subsequence relation maintaining order and supporting gaps
• Data.List.Subseq.Elem - tools for working with subsequences and Elem

Vector utilities

• Data.Vect.Equals - proof that a vector's contents are all the same
• Data.Vect.Insert - a vector insert as a data structure
• Data.Vect.More - missing vector stuff
• Data.Vect.Ordered - proof a vector is in order. WIP
• Data.Vect.Quantifiers.Fold - asserts that a proof holds for all elements relative to all successive elements.
• Data.Vect.Quantifiers.Pow - asserts that a proof holds for all elements relative to all other elements.
• Data.Vect.Set - asserts that a vector contains no duplicates by equality (slowly!)

Length-dependent Vectors

Heterogeneous vectors where the length determines the type. Including a 'powerfold' (each item is given access to all the other items in the vector).

• Data.Vect.Dependent - indexed vectors. also includes a lazy variant.
• Data.Vect.AsAt - the view of an item in an indexed vector (looks like a zipper with a current item). Includes a cartesian power(?), asAts.

Rows

Something like 'row types' (e.g. purescript), except indexed by an arbitrary key type instead of a symbol. A bit like a map, but proof-friendly.

• Data.Row - Like row types (name,value pairs), but dependent types flavoured.
• Data.Row0 - A more erased version of Data.Row.

Patricia tries

• Data.Patricia - correct by construction patricia tries. a bit unpolished

Toys

• Data.Shares - a model of how rust-style borrowing could be calculated with fractional ownership

Misc

• Data.Bool.More - xor (and ^ operator alias)
• Data.Coproduct - ad-hoc sum types
• Data.Enumerable - an interface and functions for working with types which can be fully enumerated
• Data.Erased - a holder for an erased return value
• Data.Function.More -
• Data.List.NotElem - i don't understand why but it was easier for proof search to infer
• Data.List.Elem.More - contains a relation between elements of a list?
• Data.Vect.Elem.More - what is this useful for?
• Data.Vect.Ordered - asserts that the items in a vector are all in order. not finished
• Data.Vect.Map - a map backed by a vector. is this useful? it doesn't seem to be finished.

Papers

"Simply Easy"

The original haskell paper proceeds by adding things as it goes along. I've implemented the first two versions, albeit substituting names for de bruijn indices for didactic purposes. I've also started the third, but it's still full of holes. I had to make things return Either everywhere because the haskell version is content to just drop off the end of a match - a bit naughty really.

"Ornamental algebras, algebraic ornaments"

I've implemented about half of it so far, the original is agda and i found it hard to read.

Misc

Depending on what has been accidentally committed and pushed you might find all sorts in here. Most of it will probably be PL research of some kind or another - I am working on a language.

PL Design principles

Proper errors

Rust sets a high bar here. We will take much inspiration from them.

Our main difficulty is normalisation. But I think we can sort it by keeping history of evaluated forms to provide clearer errors. The tactic language needs to be richer than idris so we can support throwing much better errors.

Change management

Loosely, haskell lets you play with all the toys and rust lets your code continue to compile. Both have drawbacks and on balance oh god i think i prefer the haskell one because i can do stuff while i wait eternity for features to stabilise. And we will be forced to be closer to haskell than rust on this one by practicalities, but why have cake if you can't eat it? So we'd like to attempt to minimise compilation breakage to avoid pissing users off.

Languages as a set of features

One thing i think haskell gets right is defining the language by the incremental addition of features which the user may then opt in to use (either by compiler flags, cabal config or compiler directives in source files). This is actually shared by PHP up to a point, strange bedfellows...

Rust also does this sort of, but once a feature is considered stable by your compiler, it starts spitting warnings about leaving the feature request in the code. In fact rust highly discourages you from using anything not yet blessed to not change forever, which you kinda need to to work around limitations in the language. It's very unsatisfactory.

In theory, features also help with alternate implementations, although the way rust does it really doesn't and the haskell is de facto a single implementation language because everyone wants ghc features to get stuff done.

I think features should probably be versioned too? We'll see. The compiler should also tell the user if it knows it's broken for a given version of a given feature in use.

Elaboration

With elaboration, we're in a comparable situation to TH, which can ask the compiler questions where rust procedural macros cannot. Thus things are immediately more likely to break since the elaborator reasonably has to work with something approximating compiler data structures.

Patching

Patching would be really nice, but i don't really know how it should work. There's nadia's stuff in coq and i hope conor will figure it out in the QTT setting. The basic idea is that when you upgrade a library, it can patch your code to use the new version.