Syntax for declarations/definitions is duplicative

[robrix]

Declarations/definitions are duplicative, which can lead to weird cases which are hard to relate to one another. For example defining the identity function like this is fine:

id : a -> a
id = \ a . a

but it’s also syntactically valid, but probably won’t typecheck, to do them in the opposite order:

id = \ a . a
id : a -> a

Edge cases like that abound, so we probably want to connect them together in the syntax.

[robrix]

Here’s a proposed syntax as applied to Base.Function:

module Base.Function

id
: (a : A) -> A
= a

const
: (a : A) -> B -> A
= a

flip
: (f : (A -> B -> C)) -> ((b : B) -> (a : A) -> C)
= f a b

fix
:  (f : (A -> B) -> A -> B)
-> (A -> B)
= f (fix f)

compose
:  (f : B -> C)
-> (g : A -> B)
-> ((x : A) -> C)
= f (g x)

and Base.Either:

module Base.Either

Either
: (L : Type) -> (R : Type) -> Type
= { A : Type } -> (L -> A) -> (R -> A) -> A

left
: { L : Type } -> { R : Type } -> (l : L) -> Either L R
= \ {_} left _ . left l

right
: { L : Type } -> { R : Type } -> (r : R) -> Either L R
= \ {_} _ right . right r

map
:  { L : Type }
-> { R : Type }
-> { R' : Type }
-> (f : R -> R')
-> ((e : Either L R) -> Either L R')
= e {Either L R'} (left {L} {R'}) (\ r . right {L} {R'} (f r))

bimap
:  { L : Type }
-> { R : Type }
-> { L' : Type }
-> { R' : Type }
-> (f : L -> L')
-> (g : R -> R')
-> ((e : Either L R) -> Either L' R')
= e {Either L' R'} (\ l . left {L'} {R'} (f l)) (\ r . right {L'} {R'} (g r))

This syntax would supersede #38.