关于语言类型系统的一些思考 #155
Description
本人才疏学浅，在此抛砖引玉。
本proposal与主页上三个问题相关，
Functional Programming， Stricter compiler， Switch statements
实施函数式编程，我建议讨论一下以下问题。
此外，如果本语言要成为一门工业界语言的话，在这个时代，我们需要一个强大的静态类型系统。
函数应当如何嵌套使用
参见 #119 . 如果我们有如下的函数调用 var e = (f (g a) b (h c d)). 当前的语言似乎必须要创建临时变量，我们可以用「其一」``「其二」``「其三」 等替代。
施「庚」於「甲」名之曰「其一」。
施「辛」於「丙」於「丁」名之曰「其二」。
施「己」於「其一」於「乙」於「其二」名之曰「戊」。
（即我们需要手动转换成ANF）
当然也可参照#99 一楼之见解写为
施「己」
於數。欲得是數，施「庚」於「甲」。
於「乙」
於數。欲得是數，施「辛」於「丙」於「丁」。
还请大家讨论最终语法。
在语言标准库方面，我们需要找到一个比较好的翻译。
如何翻译基本列操作 如 ::, map, fold, filter
另外也有一些标准的工业语言（2010年以后）基本具备的东西：
如何写类型声明 (这也和stricter compiling 有关，我们需要一个更加丰富的类型系统)
目前我们的类型系统有数 (e.g. 1)，列(e.g. [1,2])，但缺少更多的检查，例如数列([1,2])，列列([[],[2,3]])，数列列([[[],[1,2]])，列列列([[[],[2,3]],[[],[1,2]]])
从根本上来说，我们可以仿照ML或者Haskell的基本类型系统，在Type 领域需要能够表达如下的类型表达式 f :: ∀e,g. ((F a (G b) c -> H d) -> (I e -> J g))。
其中大写字母为具体的类型构造器，小写字母中的Free Variables为具体的数据类型，小写字母中的bound variable为泛型参数。
这个可表示为
吾有一術，名之曰「f」。
「f」之型如此，
欲行「f」。必先得两型，曰「e」「g」。
吾有一型，名之曰「型四」
施「G」於「b」，曰「型一」。
施「F」於「a」於「型一」於「c」，曰「型二」。
施「H」於「b」，曰「型三」。
若施於「型二」，则得「型三」，是谓「型四」之型也。
吾有一型，名之曰「型七」
施「I」於「e」曰「型五」。
施「J」於「g」曰「型六」。
若施於「型五」，则得「型六」，是谓「型七」之型也。
若施於「型四」，则得「型七」
是谓「f」之型也。
其中「f」之型如此 ... 是谓「f」之型也。 构成了顶级的类型声明。若施於x，则得y表示 x->y。 其余是谓「x」之型也的则是内部的临时变量。此法略显复杂，且书写不便。
还有一个方法则是参照#99一楼的见解，用 型...是型也。表达类型。
吾有一術，名之曰「f」。
「f」之型如此，
欲行「f」。必先得两型，曰「e」「g」。
若施於型，
若施於型，
施「F」
於「a」
於型
施「G」於「b」是型也。
於「c」。
是型也。
则得型，
施「H」於「d」是型也。
是型也。
则得型
若施於型，施「I」於「e」是型也。
则得型，施「J」於「g」是型也。
是型也。
是谓「f」之型也。
我们可以使用语法糖来简化语法（即引入多参数函数类型）。
吾有一術，名之曰「f」。
「f」之型如此，
欲行「f」。必先得两型，曰「e」「g」。
若施
於型，
若施於型，
施「F」
於「a」
於型
施「G」於「b」是型也。
於「c」。
是型也。
则得型，
施「H」於「d」是型也。
是型也。
於型，施「I」於「e」是型也。
则得型，施「J」於「g」是型也。
是谓「f」之型也。
。
举几个例子。
加法 (1+2) [加一於二]，可写为 施「加」於「一」於「二」。 此时「加」拥有如下类型：Number -> (Number -> Number)
我建议可以写为
吾有一術。名之曰「加」。
「加」之型如此，
若施於數，
则得型，
若施於數，则得數
是型也。
是谓「加」之型也。
当然，我们使用如下的语法糖。
吾有一術。名之曰「加」。
「加」之型如此，
若施
於數
於數，
则得數
是谓「加」之型也。
。
#99 的「周立」（map） 我对参数顺序稍作了修改
吾有一術。名之曰「周立」。
欲行「周立」。必先得一術。曰「转」。一列。曰「甲」。乃行是術曰。
吾有一列。名之曰「乙」。
凡「甲」中之「物」。
施「转」於「物」。名之曰「新」。充「乙」以「新」。
云云。
乃得「乙」。
是謂「周立」之術也。
以上「周立」的签名为∀a, b: (a -> b) -> [a] -> [b] 或 凡甲乙者: (甲 -> 乙) -> 甲列 -> 乙列.
吾有一術。名之曰「周立」。
「周立」之型如此，
欲行「周立」。必先得两型，曰「a」「b」。
若施
於型，若施於「a」则得「b」，是型也。
於型，施「列」於「a」，是型也。
则得型，施「列」於「b」，是型也。
是谓「周立」之型也。
欲行「周立」於「转」於「甲」，乃曰，
吾有一列。名之曰「乙」。
凡「甲」中之「物」。
施「转」於「物」。名之曰「新」。充「乙」以「新」。
云云。
乃得「乙」。
是謂「周立」之術也。
一个可以优化的地方是，我们可以诸如数列之类的词来代替施「列」於「數」，但此举似乎不适用于多参数类型构造器，例如数列列即可表示[[Number]]亦可表示列（数列）或列列（数）.
另外还有一个可以考量的地方，就是我们可以结合函数类型声明和函数声明，将两者写在一起。（其中方括号中的用字还有待考究）
吾有一術。名之曰「周立」。
欲行「周立」。必先得一[術]。曰「转」。其型曰，若施於「a」则得「b」，是型也。
一[列]。曰「甲」，其型曰施「列」於「a」，是型也。乃行是術曰。
吾有一列。名之曰「乙」。
凡「甲」中之「物」。
施「转」於「物」。名之曰「新」。充「乙」以「新」。
云云。
乃得「乙」。其型曰，施「列」於「b」，是型也。
是謂「周立」之術也。
除此以外，最新的编程语言都在引入Dependent Types 和静态验证，也就是我们需要quantification over Type Constructors，还请大家讨论我们需要采用的类型系统。
应当以怎样的方式书写ADT （包括 Record 和 Inductive Data Types）
#31 #20 已经考虑了简单的数据写法，不过该写法似乎不支持泛型。且改写法不支持Sum Types。
考虑一个简单的列类型。(GADT)
data List a = Nil | Cons a (List a)
或者dependently typed
type List a n where
nil :: a 0
cons :: a -> List a n -> List a (n+1)
因为dependent types 目前还未进入工业界，
假设我们不需要dependent type，那么
吾有一經。名之曰「列」。
欲有「列」，必先得一型，名之曰「甲」。
是經如此。
一曰 「空列」。其型如此，
施「列」於「甲」
是谓「空列」之型也。
一曰 「充」。其型如此，
若施
於「甲」
於型，施「列」於「甲」，是型也。
则得型，施「列」於「甲」，是谓「充」之型也。
是謂「列」之經也。
另外經涉及Kind，「列」的Kind是* -> *，而「数」的Kind是*。 参见 https://stackoverflow.com/questions/20558648/what-is-the-datakinds-extension-of-haskell
关于Pattern Match （即case statement）
有了 ADT 我们就需要case statement，例如我们定义以下的求和函数
-- ASSUME (+) :: Number -> Number -> Number
sum :: List Number -> Number
sum x = case x of
Nil -> 0
Cons x xs -> x + sum xs
我提议可以采用以下写法，
吾有一術。名之曰「求和」。
「求和」之型如此，
// 如果我们求和的是一个Monoid，那么可以用下面一行。但我们这里用的是数列，就不用了。
// 欲行「求和」。必先得一型，曰「a」。
若施於型，施「列」於「數」，是型也。
则得「數」。
是谓「求和」之型也。
欲行「求和」於「甲」，乃曰。
甲者，
若「空列」也，零。
若「充」施於「頭」於「尾」也，
施「求和」於「尾」，
施「加」於「頭」於其。
是謂「求和」之術也。
结语
一个强大的类型系统是较为复杂的，我开头所说的两种关于函数调用的表达式的写法，第一种可能更符合文言语法，但写起来过于复杂。第二种虽然写起来简单，却未必符合文言文法。除表达式写法外，类型系统以及和语言架构还需要进行深入讨论。此外，本语言究竟是像JS Python一样的动态语言，还是像Python Haskell一样的静态语言，还有待考量和商榷。