You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
depsterr 369044bc29 refactor 10 months ago
app refactor 10 months ago
src refactor 10 months ago
.gitignore created basic lexer 10 months ago initialized a cabal enviornment 10 months ago
LICENSE initialized a cabal enviornment 10 months ago
Setup.hs initialized a cabal enviornment 10 months ago
TODO it, it works? 10 months ago
readme.simple.txt refactor 10 months ago
readme.txt complete conversion to simpler subset ast 10 months ago
sexprml.cabal refactor 10 months ago


-- {-
-- Haskell style comments with {- -} and --
-- -}

-- Full UTF-8 support

-- Lazy

-- Types are given explicitly with [TYPE]\s+(EXPR) or inferred in the case of (EXPR)

-- Declerations are defined with the def keyword, which binds the name in the current
-- enviornment (shadowing any existing binding of the same name.

-- Type quantification is done explicitly and binds the type variables in the scope,
-- that is to say, if we were to make a local definition we could write A, B or C in
-- it's type signature. If one where to write ∀ A B C however, this would shadow the
-- existing bindings.
[∀ A B C : (B → C) → (A → B) → A → C]
(def (compose f g x) (f (g x)))

-- Much like in haskell one can pattern match in the following manner.
[𝔹 → 𝔹]
(def (((not 𝕋) 𝔽)
((not 𝔽) 𝕋)))

-- In general one can make multiple definitions in this manner, however, any explicit type
-- signature will only apply to the first definition. Of course all patterns for a function
-- must result in the same type as the first one.

-- Pattern matching can also be done by matching with case. A case statement MUST match all
-- possible patterns of constructors (ofcourse, wildcard and catch-all statements are allowed).
[𝔹 → 𝔹]
(def (not b) (case b (𝕋 𝔽)
(𝔽 𝕋)))

-- Pattern matching on N arguments desugars into matching on a case tree.
[∀ A B : 𝕄 A → 𝕄 B → 𝔹]
(def (((allJust (𝑱 _) (𝑱 _)) 𝕋)
((allJust _ _) 𝔽)))

-- Function definition desugars to binding to a lambda
[𝔹 → 𝔹]
(def not (λ b (case b (𝕋 𝔽)
(𝔽 𝕋))))

-- If you would wan't do write this lambda yourself you'll probably want to use a lambda case
-- which, of course, de sugars to the previous snippet.
[𝔹 → 𝔹]
(def not (λcase (𝕋 𝔽)
(𝔽 𝕋)))

-- Data declerations are done as follows
(data 𝔹 ([𝔹]𝕋)

-- A more complex example is the List type. Here the initial (List A) binds the type variable
-- A which is then used when defining the constructors. The constructors are defined using
-- the same syntax as in agda (or haskell with the GADTsyntax language extension).
-- Note that the uppercase starting letter is a style choice and completely optional.
(data (List A) ([List A] Empty)
([A → List A] Cons))

-- Type synonyms are defined as functions in type space. Note that type space functions are
-- heavily limited. Any function which takes or returns a Type may not take or return any
-- other type than Type or other functions over Types.
(def Bool 𝔹)

[Type → Type]
(def (Maybe A) (𝕄 A))

[(Type → Type) → Type → Type]
(def (Apply M A) (M A))

-- The N-ple type is special in that it is defined for any N, however, since this is not
-- a dependently typed language this is not parameterised, instead the types 2pl 3pl 4pl,
-- and so on are generated as needed by the compiler when used in source. In general they
-- are defined as follows.
(data (Npl A1 A2 A3 ... AN)
([A1 → A2 → A3 → ... → AN → Npl] Npl))

-- Not only do we use GADT syntax, we also support GADTs! Here is the classic example where
-- type refinement over the quantified variable A in eval is done by pattern matching on
-- constructors of T which make A explicit.
(data (T A) ([Int → T Int] lit)
([T Int → T Int] suc)
([T Int → T Bool] zero?)
([T Bool → T a → T a → T a] if)
([T a → T b → T (a, b)] pair))

[∀ A : T A → T A]
(def eval (λcase ((lit i) (i))
((suc i) (+ 1 (eval i)))
((zero? i) (eq 0 (eval i)))
((if b x y) (if (eval b) (eval x) (eval y)))
((pair x y) (2pl x y))))

-- Type generic programming can be done with type classes. Type classes and their instances
-- are defined much like in haskell, however they behave more like instance records in agda.
-- That is, a type class is simply a parameterised datatype, meaning type instances are simply
-- terms of this type. In order to keep the utility of type classes the compiler will itself pick
-- an existing instance when a function needing it is called, however if more than one instance
-- is in scope the user will have to supply it explicitly. This nicely solves the issue you see in
-- haskell where there are multiple instances that make sense for one type (e.g the Integer monoid)
-- in which case they resort to using newtypes to seperate the instances.

-- A class (or record) is defined in the following manner, which should feel somewhat familiar.
(record (Monoid A) ([A] ident)
([A → A → A] <>))
-- Perhaps one would expect the constructors to have the type [A → Monoid A] and
-- [(A → A → A) → Monoid A], however this would be nonsensical as the record only has a single
-- actual constructor, and what we specify are the types needed to construct it. The definition
-- above brings the following into scope:
-- [∀ A : Monoid A ⇒ A]
-- ident
-- [∀ A : Monoid A ⇒ A → A → A]
-- <>

-- Here the ⇒ arrow is introduced. The ⇒ arrow is much like the → arrow, except it marks the left
-- parameter as implicit, that is, it expects the compiler to provide it. Implicit arguments can be
-- given explicitly by wrapping them in curly braces {EXPR}. Here is an example:

-- An instance is defined as follows
[Monoid Int]
(def Sum (instance (ident 0)
(<> +)))

-- Note that we (just like in haskell) can use constraints to define general instances.
[∀ A : Eq A ⇒ List A → List A → 𝔹]
(def (((listEq Empty Empty ) 𝕋)
((listEq (Cons a as) (Cons b bs)) (&& (eq a b) (listEq as bs)))
((listEq _ _ ) 𝔽)))

[∀ A : Eq A ⇒ Eq (List A)]
(def LEQ (instance (eq listEq)))

-- If we then have Product and Sum instance we can do the following
[∀ F A : Foldable F ⇒ Monoid A ⇒ F A → A]
(def mconcat (foldr <> ident))

-- There is also a more generalised verision of partial application. By placing a wildcard _
-- in the place of an argument to a function you partially apply it. For example. If you have a
-- 5pl of the type 5pl A B C D E F then (5pl a b _ d _ f) (where a b d and f are bound variables
-- of the correct type) is of the type (C → E → 5pl A B C D E F). In other words
-- (f a _ c _ e)
-- desugars to
-- (λ b d (f a b c d e))

-- let ... in
(def (q x)
(let (x₂ (+ 1 1))
(x₁ (+ 1 2))
in (+ x x₁ x₂)))