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

lens
Lenses, Folds, and Traversals  Join us on web.libera.chat #haskelllens 
semanticsource
Parsing, analyzing, and comparing source code across many languages 
codebuilder
Packages for defining APIs, running them, generating client code and documentation. 
text
Haskell library for space and timeefficient operations over Unicode text. 
compendiumclient
Mu (μ) is a purely functional framework for building micro services. 
cassava
A CSV parsing and encoding library optimized for ease of use and high performance 
unorderedcontainers
Efficient hashingbased container types 
holmes
A reference library for constraintsolving with propagators and CDCL. 
binary
Efficient, pure binary serialisation using ByteStrings in Haskell. 
primitive
This package provides various primitive memoryrelated operations. 
resourcepool
A highperformance striped resource pooling implementation for Haskell 
jsonautotype
Automatic Haskell type inference from JSON input 
audiovisual
Extensible records, variants, structs, effects, tangles 
discrimination
Fast linear time sorting and discrimination for a large class of data types 
dependentmap
Dependentlytyped finite maps (partial dependent products) 
dependentsum
Dependent sums and supporting typeclasses for comparing and displaying them 
IORefCAS
A collection of different packages for CAS based data structures. 
safecopy
An extension to Data.Serialize with builtin version control 
bifunctors
Haskell 98 bifunctors, bifoldables and bitraversables 
streaming
An optimized general monad transformer for streaming applications, with a simple prelude of functions 
orgmodeparse
Attoparsec parser combinators for parsing orgmode structured text! 
protobuf
An implementation of Google's Protocol Buffers in Haskell. 
reflection
Reifies arbitrary Haskell terms into types that can be reflected back into terms 
uuidtypes
A Haskell library for creating, printing and parsing UUIDs 
scientific
Arbitraryprecision floatingpoint numbers represented using scientific notation
Collect and Analyze Billions of Data Points in Real Time
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).