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

unboundgenerics
Specify variable binding in syntax trees using GHC.Generics (reimplementation of Unbound) 
languageconf
languageconf  .conf (e.g. nginx configuration) parsers and prettyprinters for the Haskell programming language.
InfluxDB  Power RealTime Data Analytics at Scale
* Code Quality Rankings and insights are calculated and provided by Lumnify.
They vary from L1 to L5 with "L5" being the highest.
Do you think we are missing an alternative of caledon or a related project?
README
Caledon Language
Caledon is a dependently typed, polymorphic, higher order logic programming language. ie, everything you need to have a conversation with your computer.
Background
This is part of my masters thesis. Feedback would be appreciated. Considering this, it is still in the very early research stages. Syntax is liable to change, there will be bugs, and it doesn't yet have IO (I'm still working out how to do IO cleanly, but this WILL come).
It's named caledon after the "New Caledonian Crow"  a crow which can make tools and meta tools. Since this language supports meta programming with holes, implicits, polymorphism, and dependent types, I thought this crow might be a good mascot. Also, file extensions are ".ncc"
This language was inspired by twelf, haskell and agda.
Goals
Make logic programming less repetative
A logic programming language that is good at defining DSLs
A language/system for conversing with the machine in a manner less one sided and instructional than regular programming.
Make automated theorem proving intuitive.
Philosophies
Metaprogramming should be easy and thus first class.
User facing code should not crash  runtime code should be type checked.
Metacode should be optionally typechecked, but well type checked.
Metaprogramming should not require AST traversal.
Your programming language should be turing complete  totality checking is annoying.
Syntax should be elegant.
Primitives should be minimal, libraries should be extensive. Learning a culture is easy if you speak the language. Learning a language by cultural immersion isn't as trivial.
Usage
 To install from hackage:
> cabal install caledon
 To install directly from source:
> git clone git://github.com/mmirman/caledon.git
> cd caledon
> cabal configure
> cabal install
 To run:
> caledon file.ncc
 Unicode syntax is possible in emacs using:
Mx \ TeX <ENTER>
Features
 Logic programming: Currently it uses a breadth first proof search. This is done for completeness, since the proof search is also used in type inference. This could (and should) possibly change in the future for the running semantics of the language.
defn num : prop
 zero = num
 succ = num > num
defn add : num > num > num > prop
 add_zero = add zero N N
 add_succ = add (succ N) M (succ R) < add N M R
 we can define subtraction from addition!
defn subtract : num > num > num > prop
as \a b c : num . add b c a
 Some basic IO: Using unix pipes, this Caledon can be used more seriously. Somebody plz write a wrapper?
query main = run $ do
, putStr "hey!\n"
, readLine (\A . do
, putStr A
, putStr "\nbye!\n")
 Higher order logic programming: like in twelf and lambdaprolog. This makes HOAS much easier to do.
defn trm : prop
 lam = (trm > trm) > trm
 app = trm > trm > trm
 we can check that a term is linear!
defn linear : (trm → trm) → prop
 linear_var = linear ( λ v . v )
 linear_lam = {N} linear (λ v . lam (λ x . N x v))
← [x] linear (λ v . N x v)
 linear_app1 = {V}{F} linear (λ v . app (F v) V)
← linear F
 linear_app2 = ?∀ V . ?∀ F . linear (λ v . app F (V v))
← linear V
 Calculus of Constructions: This is now consistent, and still has similar expressive power! Now any term must be terminating. Although term/proof search might not be terminating, proof search can be used to search more intelligently for theorems in the term language.
defn maybe : prop → prop
 nothing = maybe A
 just = A → maybe A
infix 1 =:=
defn =:= : A > A > prop
 eq = (=:=) {A = A} V V
infix 0 /\
defn /\ : prop > prop > prop
 and = {a : prop}{b : prop} a > b > a /\ b
infixr 0 >
defn > : [a : prop] [b : prop] prop
as \a : prop . \b : prop . [ha : a] b
 Optional Unsound declarations: Embedding certain terms has never been easier! This way you can create recursive type definitions such as the well known "prop : prop".
unsound tm : {S : tm ty} tm S → prop
 ty = tm ty
 ♢ = tm ty > tm ty
 Π = [T : tm ty] (tm T → tm T) → tm $ ♢ T
 lam = [T : tm ty][F : tm T → tm T] tm {S = ♢ T} (Π A : T . F A)
 raise = {T : tm ty} tm T → tm $ ♢ T
Indulgent type inferring nondeterminism: The entire type checking process is a nondeterministic search for a type check proof. This could be massively slow, but at least it is complete. The size of this search is bounded by the size of the types and not the whole program, so this shouldn't be too slow in practice. (function cases should be small). I'm working on adding search control primitives to make this more efficient.
Holes: types can have holes, terms can have holes. The same proof search that is used in semantics is used in type inference, so you can use the same computational reasoning you use to program to reason about whether the type checker can infer types! Holes get filled by a proof search on their type and the current context. Since the entire type checking process is nondeterministic, if they get filled by a wrong term, they can always be filled again.
defn fsum_maybe : (A > B > prop) > maybe A > maybe B → prop
 fsum_nothing = [F : A > B > prop] maybe_fsum F nothing nothing
 fsum_just = [F : _ > _ > prop][av : A][bv : B]
maybe_fsum F (just av) (just bv)
< F av bv
 Implicit arguments: These are arguments that automagically get filled with holes when they need to be. They form the basis for typeclasses (records to be added), although they are far more general. This is also where the language is most modern and interesting. I'm curious to see what uses beyond typeclasses there are for these.
defn functor : (prop → prop) → prop
 isFunctor = ∀ F . ({a}{b : _ } (a → b → prop) → F a → F b → prop) → functor F.
defn fsum : {F} functor F => {a}{b} (a → b → prop) → F a → F b → prop
 get_fsum = [F] functor F > [FSUM][Foo][Fa][Fb] FSUM Foo Fa Fb > fsum Foo Fa Fb
defn functor_maybe : functor maybe > prop.
 is_functor_maybe = functor_maybe (isFunctor fsum_maybe).
 this syntax is rather verbose for the moment. I have yet to add typeclass syntax sugar.
 Nondeterminism control: You can now control what patterns to match against sequentially versus concurrently. This gives you massive control over program execution, and in the future might be implemented with REAL threads!
defn runBoth : bool > prop
> run0 = runBoth A
< putStr "tttt "
< A =:= true
 run1 = runBoth A
< putStr "vvvv"
< A =:= true
 run2 = runBoth A
< putStr "qqqq"
< A =:= true
> run3 = runBoth A
< putStr " jjjj"
< A =:= false
query main = runBoth false
 main should print out something along the lines of "tttt vvqvqvqq jjjj"
 Arbitrary operator fixities: combined with the calculus of constructions, you can nearly do agda style syntax (with a bit of creativity)!
defn bool : prop
 true = bool
 false = bool
defn if : bool > bool
as \b . b
infix 1 :
defn : : {a : prop} a > a > (a > a > a) > a
as ?\t : prop . \a b. \f : t > t > t. f a b
infix 0 ==>
defn ==> : {a : prop} bool > ((a > a > a) > a) > a > prop
 thentrue = [f : _ > A] (true ==> f) (f (\a b : A. a))
 thenfalse = [f : _ > A] (false ==> f) (f (\a b : A. b))
defn not : bool > bool > prop
as \v . if v ==> false : true
 Optional unicode syntax: Monad m ⇒ ∀ t : goats . m (λ x : t . t → t).
 implication : "a > b" or "a → b" or "a < b" or "a ← b"
 implicits: "a => b" or "a ⇒ b" or "a <= b" or "a ⇐ b"
 Quantification: "[x:A] t" or "∀ x:A . t" or "forall x:A . t"
 abstraction: "λ x . t" or "\x.t"
 Quantified implicits: "{x:A} t" or "?∀ x:A . t" or "?forall x:A . t"
 implicit abstraction: "?λ x . t" or "?\x.t"
Primary Contributers
Author: Matthew Mirman
Advisor: Frank Pfenning
Secondary Contributers
Samuel Gélineau (gelisam)
Devin Nusbaum (eldevo)