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
c195c8a926

10 months ago  

app  10 months ago  
src  10 months ago  
.gitignore  10 months ago  
CHANGELOG.md  10 months ago  
LICENSE  10 months ago  
Setup.hs  10 months ago  
TODO  10 months ago  
readme.simple.txt  10 months ago  
readme.txt  10 months ago  
sexprml.cabal  10 months ago 
readme.txt
 {
 Haskell style comments with { } and 
 }
 Full UTF8 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 catchall 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.
[Type]
(def Bool 𝔹)
[Type → Type]
(def (Maybe A) (𝕄 A))
[(Type → Type) → Type → Type]
(def (Apply M A) (M A))
 The Nple 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
[idk]
(def (q x)
(let (x₂ (+ 1 1))
(x₁ (+ 1 2))
in (+ x x₁ x₂)))