unfixbinders alternatives and similar packages
Based on the "Data" category.
Alternatively, view unfixbinders alternatives based on common mentions on social networks and blogs.

streaming
An optimized general monad transformer for streaming applications, with a simple prelude of functions
InfluxDB  Purpose built for realtime analytics at any scale.
Do you think we are missing an alternative of unfixbinders or a related project?
README
Peppermint Prover
A fresh interactive theorem prover
(Also home of the [unfixbinders](unfixbinders/) library for a while)
Why
The world certainly doesn't need another proof assistant. There are plenty great ones out there for all your computerchecked proving needs (such as [Coq][coq], [Isabelle][isabelle], [Agda][agda], or [Lean][lean], to name a few). To be perfectly blunt: I simply needed a side project, and I happen to like writing and designing proof assistants.
I've been thinking of dependently typed linear logic [for a while][dissectl]. My interest was greatly revived by Michael Schulman's [remarkable analysis][llconstructivemaths] of the connection between linear logic and the constructive mathematics praxis.
On the choice of foundation
I favour dependent type theory over more traditional logics, such as HOL, mainly for one reason: I like to abstract all the things, and dependent type theory offers a framework to do just that.
Design
Language
The language basically follows [my ideas][dissectl] on dependent linear types, though [McBride's][mcbriderig] and [Atkey's][atkeyqtt] more recent work on socalled quantitative type theory greatly improve the theory. I'm following the style of [Linear Haskell][linearhaskell] rather than that of quantitative type theory because I believe it to work better. However, it seems to me that values (of positive type) should maybe have a forward analysis in the style of quantified type theory, rather than the backward analysis that computations (of negative types) seem to require.
Putting these preliminary thoughts together, Peppermint
 is a sequent calculus (based on system L), because
 Sequent calculus is closer to interactive proofs than natural deduction, hence basic tactics will be easier to write
 I learnt from [Lengrand][lengrandthesis] that dependently typed unification is made significantly easier in sequent calculus
 I believe sequent calculus to be a sturdier (and, I confess, more fun) foundation than natural deduction
 is based on "classical" linear logic (that is, it sports an involutive
dualisation operations)
 This is needed in Schulman's analysis (though Schulman's logic is affine, and I'm not entirely sure yet how the analysis carries over to proper linear logic)
 has dependent elimination. In particular Πtypes are inhabited by
linear functions.
 Without dependent elimination most of the properties of dependent type I'm interested in for reasoning disappear
 is polarised (that is values have positive types and computations
have negative types), with explicit shifts. Like callbypushvalue,
variables only have positive types.
 It seems to solve many problems related to linear dependent elimination, especially in presence of duality.
 On the other hand it makes it less obvious how to have judgemental computations. It's part of the exploration goals to try and pin this down.
 has anonymous least and largest fixed point construction for types
(respectively, anonymous recursive terms).
 It certainly comes with its own set of problems (mostly inscrutable type error messages), but it's cheaper to implement (plus, it fits better the implementation philosophy below).
 It should make it easier to write typegenerating code (such as Coq's [parametricity plugin][coqparametricity]).
Clearly the design is not particularly justified, mostly it's what I want to do, rather than what needs to be done. So be it.
Some nonlogic considerations:
 Peppermint is an interactive prover in the style of [Coq][coq] in that proofs are elaborated with a tactic language
 The tactic language is an extension of the Peppermint logical language
 Peppermint terms (proofs and types) can contain holes aka
metavariables aka existential variables. These holes can play
various roles (to be automatically solved by the type inference
mechanism, to be elaborated by interactive proofs, …), as a
consequence holes have structure (I call it the hole language) which
allows to specify what the programmer expects of the hole.
 For instance the programmer can specify that the hole under
consideration must be solved by a particular tactic
t
(I believe [Idris][idris] has something like this, too)
 For instance the programmer can specify that the hole under
consideration must be solved by a particular tactic
Implementation
As a general consideration, I don't have an enormous amount of time to dedicate to this project, so I favour everything that can gain me some time. I intend this project to be innovative and exploratory only on the narrow set of aspects such as the logic and, to some degree, the logic's implementation.
For the rest, I will prefer offtheshelf components. I'll also try to use bidirectional parser/prettyprinter rather than give myself a lot of flexibility on either end. I also favour types and structure over efficiency. Incidentally, it's also why this program is written in the Haskell programming language: while for a more largescale effort I would probably prefer Ocaml, Haskell is unique in the shortcuts it offers, and will more realistically get Peppermint off the ground.
To sketch a more detailed design of the implementation, Peppermint is implemented as various layers, each concerned with extending the logic with extra stuff. At this early stage, I don't have yet a precise run down of the specific layers that Peppermint will have (or the API of Peppermintthelibrary). But, here are some example of layers:
 The very bottom layer only understands a single expression. There is no way to break an expression into several toplevel definitions. There are letbinders, of course, but that's about all. This layer can only typecheck terms.
 Definitions are added in a further layer. But we can only typecheck definition at this point.
 A further layer will add existential variables and type inference.
A layer can add elements which are recursive with previous layer elements (e.g. adding letbinders to a layer that only understands lambdas), because they are defined by open recursion (that is, recursive types are defined as the least fixed point of a functor which is materialised, and functions which would normally recurse over that type are defined as algebra of the structure functor).
I intend the peppermint executable to give access to several (but probably not all) of the layers.
As a last note: it is not the intention that the proofs always be verified by the lowest layer. This is a point on which the design differs radically than that of [Coq][coq]. In particular, proofs interactively elaborated, by tactics, as terms with existential variables are not rechecked in a notional kernel at "qed" time. I am, however, considering giving the possibility of translating developments from a layer to lower layers, for the sake of heightened confidence (it is not, however, necessary, that all features which are not in the lowest layer can be eliminated).