本指南假设读者熟悉OCaml和Twelf,本快速入门指南将快速准确地介绍豫言。 豫言文件以"。豫"为结尾。 豫言的数据类型描述采用了Twelf结构,函数定义采用了Twelf和Haskell相结合的结构。
豫言文件是一系列用句号(。)分隔的语句。圆括号(())可以被添加在任意地方表示结合性,方括号(「」)用来表示名称,若无歧义,圆括号和方括号都可以省略。引号(『』)用来表示字符串。
每个文件的开头需要有一行"寻观标准库之书。"
函数使用(OCaml中的空格符)在豫言中用于
来表示。例如,加法add x y
在豫言中写为add于x于y
。豫言提倡使用中文,所以加 甲 乙
(等同于(加 甲) 乙
)在豫言中可以被写成「加」于「甲」于「乙」
,除非有歧义,所有的括号都可以省略,因而可以写成加于甲于乙
。
豫言中大量使用了操作符,例如_+_
在豫言中则为〇加〇
,故3 + 2
在豫言中可以写成三加二
。
因为操作符的优先级有些复杂,我们推荐在不明确操作优先级的情况下嵌套使用操作符时使用括号,例如3 + 2 * 1
推荐写成三加(二乘一)
。请注意,这里不可以写三加「二乘一」
,因为「二乘一」
会被理解成变量名。
List.length => 长度 [] => 【】 :: => 〇衔〇 + => 〇加〇 = => 等于 List.append => 「附加」 List.nth => 第N个 (例子:第N个于零于「甲列」) true => 阳 false => 阴
语法结构也遵循着一定的对应关系,比如if true then 2 else 3
在豫言中写为若阳则二否则三
,
我们把这个语法结构记为
if _ then _ else _ ==> 若 〇 则 〇 否则 〇
注意,豫言中所有的空格都可以省略。
下面是OCaml中一些常用的语法结构和他们对应的豫言表示(以及对应的例子)。
match _ with _ => _ | ... | _ => _
==>
鉴〇而 有〇则〇 或 ... 或有〇则〇
match (f x) with 0 => true | _ => false
==>
鉴(艾弗于艾克斯)而 有零则阳 或有「其他数」则阴
_ -> _ ==> 化〇则〇
int -> bool ==> 化整数而爻
bool -> string ==> 化爻而字符串
int -> int -> bool ==> 化整数而整数而爻
fun _ -> _ ==> 会〇而〇
fun x -> x + x ==> 会甲而甲加甲
let rec _ : _ = _
==>
〇乃〇也。 〇者〇也。
let rec f : int -> int = fun x -> x + 1
==>
艾弗乃化整数而整数也。 艾弗者会甲而甲加一也。
类型参数采用类似System F的系统表示,'a list的意思是名为list
的类型构造函数调用,参数是'a
。
'a list -> 'a list
的含义是{a : Type} list a -> list a
。
比如
_list ==> 〇列
int list ==> 整数列
{_ : Type} _ ==> 承〇而〇
{x : Type} f x ==> 乘艾克丝而艾弗于艾克丝
{x : Type} {y : Type} f x -> g y ==> 承艾克丝而承吾艾而化艾弗于艾克丝而吉于吾艾
let rec length : 'a list -> int = fun x -> match x with [] -> 0 | (head :: tail) -> 1 + length tail
==>
长度乃乘甲而化甲列而整数也。 长度者会甲而 鉴甲而 有【】则零 或有「头」衔「尾」则一加(长度于尾)也。
数据结构的定义用〇立〇也
来表示。这个表示方式很像Twelfth或者GADT的格式。
举例
type bool = true | false
==>
爻立元类型也。 阳立爻也。 阴立爻也。
type 'a option = None | Some of 'a
==>
可选值立化元类型而元类型也。 可无立承甲而元类型于甲也。 可有立承甲而化甲而元类型于甲也。
type 'a list = [] | :: of 'a * 'a list
==>
「〇列」立化元类型而元类型也。 【】立承甲而甲列也。。 「〇衔〇」立承甲而化甲而化甲列而甲列也。
Claude/GPT,你的任务是:
我在给我的编程语言写快速入门文档,目标是Claude3或者GPT4看了我的文档后的代码写作水平可以接近Python,请告诉我文档的不足之处,我愿意改进文档。文档的提升建议请具体一点,你觉得你的豫言水平和Python比怎么样?请举出一个可以用豫言也可以用Python实现的例子,再举一个Python可以实现但豫言实现不了得例子。