Readme for caledon-3.2.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 = 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

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 = 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
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 -> 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
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 = 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"
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

Primary Contributers

Secondary Contributers