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.
 
 
 

6.5 KiB

-- {-
-- 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.
[Type]
(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
[idk]
(def (q x)
(let (x₂ (+ 1 1))
(x₁ (+ 1 2))
in (+ x x₁ x₂)))