rust-lisp

This was made to help me practice PLD/I concepts as I learn them.

Language Goals

• Complete Static Type Inference
• Sound Type System
• Type Erasure
• Compiled (!?)

Implies

• No Dependent Types

Current Syntax Spec

;; lambda (expr expr)
(x -> x)
;; bind
(x <- 3)
((double x) <- (+ x x)) 
;; theoretically desugars to: (double <- (x -> (+ x x)))

todo:

1. Create namespace for datatypes and traits (including ->)
2. Add datatypes
3. Add an if
4. Imports/modules
5. Out of Order Declaration
6. pattern matching
7. Work on a compiler?
8. Add atoms? (:hi)

(Eventual) Spec for Datatypes

;; type fn literal is only allowed in data/trait declarations 
;; and their respective constructors/signatures
(-> Nat Nat Nat) ;; type of +

;; type constructors are type function bindings to a new closed type
(data Bool Type
      (T <- Bool)
      (F <- Bool))

;; data polymorphism, captured vars are types 
;; (because constructors are type functions (no dependent types))
(data Hmm (-> Type Type)
      (Nah <- (Hmm a))
      ((Yah a) <- (Hmm a)))

;; type and constructor names may clash
(data , (-> Type Type Type)
      ((, a b) <- (, a b)))

;; data is recursive
(data List (-> Type Type)
      ([] <- (List a))
      ((: a (List a)) <- (List a)))

;; data is a GADT
(data AST (-> Type Type)
      ((Lit a)                   <- (AST a))
      ((Add (AST Nat) (AST Nat)) <- (AST Nat))
      ((Eql (AST a) (AST a))     <- (AST Bool)))

On Type Aliases

Ideally, this is totally unnecessary. Currently it's unusable.

Right now there are no type hints. I think if binding level typings are allowed, we can add this.

(type (AggFn a) (-> a a a)))
((AggFn a) <~ (-> a a a))) ;; mirrors inf type err msg T0 !~ T1
((AggFn a) :: (-> a a a)))
((AggFn a) <-> (-> a a a)))

to brainstorm:

1. kind syntax? (=> (Num a) (Show a) (-> a a (IO a)))

Syntax Experiments

(($ f x) <- (f x))
((. f g x) <- (f (g x)))
((flip f y x) <- (f x y))

(data , (-> Type Type Type)
    ((, a b) <- (, a b))
    )    

((uncurry f (, a b)) <- (f a b))

((fst (x, _)) <- x)
((snd (_, x)) <- x)

(data State (-> Type Type Type)
    ((State (-> s (, a s)))
        <- (State s a)))

((run (State fsas) s) <- (fsas s))

;; (trait <trait name> <kind argument (a type)>
;;      <method binding>...
;;      )

(trait Monad (-> Type Type)
    ((>>=    (m a) (-> a (m b))) <- (m b))
    ((>>     (m a) (m b))        <- (m b))
    ((return a)                  <- (m a))
    )

(impl Monad (State s)
    ((>>= sa famb) <- 
        (State (. (uncurry (. run famb)) (run sa))))
    ((>> sa sb) <-
        (State (. (run sb) (. snd (run sa)))))
    (return <- (. State (,)))
    )

(data Hmm (-> Type Type)
    (Nah <- (Hmm a))
    ((Yah a) <- (Hmm a))
    )

(impl Monad Hmm
    ((>>= ma famb) <- 
        (match ma 
            (Nah -> Nah) 
            ((Yah x) -> (Yah (famb x)))
            )
        )
    (>> <- const)
    (return <- Yah)
    )

(data Identity (-> Type Type) ((Id a) <- (Identity a)))

(impl Monad Identity 
      (>>= <- (flip $))
      (>> <- const)
      (return <- Id)
      )