The caledon package

[Tags: gpl, program]

a dependently typed, polymorphic, higher order logic programming language based on the calculus of constructions designed for easier metaprogramming capabilities.


[Skip to ReadMe]

Properties

Versions0.0.0.0, 2.0.0.0, 2.1.0.0, 2.1.1.0, 3.0.0.0, 3.1.0.0, 3.2.0.0, 3.2.1.0
Change logNone available
Dependenciesbase (>=4.0 && <5.0), containers (>=0.4 && <1.0), mtl (>=2.0 && <3.0), parsec (>=3.0 && <4.0), transformers (>=0.3 && <1.0) [details]
LicenseGPL-3
AuthorMatthew Mirman
MaintainerMatthew Mirman <mmirman@andrew.cmu.edu>
CategoryLanguage, Interpreter
Home pagehttps://github.com/mmirman/caledon
Source repositoryhead: git clone git://github.com/mmirman/caledon.git
Executablescaledon
UploadedFri Mar 8 01:35:18 UTC 2013 by MatthewMirman
Downloads1318 total (70 in last 30 days)
Votes
2 []
StatusDocs not available [build log]
Successful builds reported [all 2 reports]

Downloads

Maintainers' corner

For package maintainers and hackage trustees

Readme for caledon-2.1.1.0

Caledon Language logo

Caledon is a dependently typed, polymorphic, higher order logic programming language. ie, everything you need to have a conversation with your computer.

Background

Goals

Philosophies

Usage

> cabal install caledon
> git clone git://github.com/mmirman/caledon.git
> cd caledon
> cabal configure
> cabal install
> caledon file.ncc
M-x \ TeX <ENTER>

Features

defn num  : prop
   | zero = num
   | succ = num -> num

defn add  : num -> num -> num -> prop
   | add_zero = [N] add zero N N
   | add_succ = [N M R] 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

query main = run $ do 
                 , putStr "hey!\n"
         , readLine (\A . do 
         , putStr A
                 , putStr "\nbye!\n")
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
defn maybe   : prop → prop
   | nothing = {a} maybe a
   | just    = {a} a → maybe a

infix 1 =:=
defn =:= : {a : prop} a -> a -> prop
   | eq = {a : prop} a =:= a

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
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
defn fsum_maybe  : {a}{b} (a -> b -> prop) -> maybe a -> maybe b → prop
   | fsum_nothing = {a}{b}[F : a -> b -> prop] maybe_fsum F nothing nothing
   | fsum_just    = {a}{b}[F : _ -> _ -> prop][av : a][bv : b]
                   maybe_fsum F (just av) (just bv)
                   <- F av bv
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.
defn runBoth : bool -> prop
  >| run0 = [A] runBoth A 
                <- putStr "tttt "
                <- A =:= true

   | run1 = [A] runBoth A
                <- putStr "vvvv"
                <- A =:= true

   | run2 = [A] runBoth A
                <- putStr "qqqq"
                <- A =:= true

  >| run3 = [A] runBoth A
                <- putStr " jjjj"
                <- A =:= false

query main = runBoth false

-- main should print out something along the lines of "tttt vvqvqvqq jjjj"
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 =  [a:prop][f : (a -> a -> a) -> a] (true ==> f)  (f (\A B. A))
   | thenfalse = [a:prop][f : (a -> a -> a) -> a] (false ==> f) (f (\A B. B))

defn not : bool -> bool -> prop
  as \v . if v ==> false |:| true