### Speaker

Zhichu Chen
(Shanghai Advanced Research Institute)

### Description

Functional programming guarantees the correctness of the output. A system written in statically typed language, such as `Haskell`

, not only benefits from the type-safe property, but can also use the powerful **generic algebraic data type** (GADT). Furthermore, languages implementing dependent types, e.g., `idris`

, can serve as a theorem proofer, making the whole system total and elegant.

In this article, the author will use `Haskell`

to demonstrate the process of editing. Some interesting details are shown:

- parsing an article source file (
`LaTeX`

or`MS Word`

) to an**abstract syntax tree**(AST), which can be edited and further parsed back for review; - using patch theory to selectively merge modifications submitted by the editor and the author
*without*informing each other; - function composition: define function fragments and compose them into real programs.

\begin{align}

f_1 &= \ldots \qquad \text{(read from \LaTeX)} \

f_2 &= \ldots \qquad \text{(read from WORD)} \

g &= \ldots \qquad \text{(display AST in HTML for editing)} \

h_1 &= g \circ f_1 \

h_2 &= g \circ f_2 \

\end{align}

### Primary author

Zhichu Chen
(Shanghai Advanced Research Institute)