Type system idea for Carrot.

carrot-idea.carrot.lisp

(interface ICallable
           (as-function a (Fn b c)))

(interface IBool ICallable
           (if IBool a a a))

(implements True IBool
            true)
(= (if True a a a)
   _ then else then)
(= (as-function True (Fn a a a))
   _ (^ x y x))

(implements False IBool
            false)
(= (if False a a a)
   _ then else else)
(= (as-function False (Fn a a a))
   _ (^ x y y))


(interface (IOption a)
           (pull  (IOption a) a)
           (>>=   (IOption a) (Fn a (IOption a)) (IOption a))
           (none? (IOption a) Bool))

(implements None (IOption a)
            none)
(= (none? None) true)
(= (>>= None (Fn a (IOption a)) None) _ _ None)


(implements (Opt a) (IOption a)
            (some :val a))
(= (none? (Opt a)) false)
(= (pull (Opt a) a) o (get o :val))
(= (>>= (Opt a) (Fn a (Opt a)) (Opt a))
   o f (f (pull o)))


(interface (IList a)
           (car  (IList a) a)
           (cdr  (IList a) (IList a))
           (nil? (IList a) IBool))

(implements Nil (IList a) IBool nil)
(= (nil? Nil) true)
(= (if Nil a a a)
   _ then else else)

(implements (List a) (IList a)
            (cons :car a :cdr (IList a)))

(= (car (List a) a)
   xs (get xs :car))
(= (cdr (List a) (IList a))
   xs (get xs :cdr))
(= (nil? (List a) Bool) _ false)


;;;;implementations can have missing definitions. type error is signaled only when the missing definition is used