Defining Desk-lang

[hsk]

日本語で大丈夫ですか？

[ryo33]

I've written the syntax of term, but I don't know a nice OCR software for it, so I post it here as is.

[ryo33]

実用的にすることを考えると繰り返しの中ではカンマをオプショナルで使えるようにしたいです。

[hsk]

{T}  : empty or more repetitions separated by optional commas (trailing comma is valid)

term = NAT                                               // natural number
        | "<" { term } ">"                                   // prod
        | "[" { term } "]"                                    // vec
        | "{" { term "=>" term } "}"                          // map
        | "λ" type "->" term                                // function
        | "@" IDENT term                                    // label
        | "@@" IDENT term                                   // brand
        | "branch" term "{" { type "=>" term } "}"          // branch
        | "let" term "in" term                              // let
        | "&" type { term }                                   // ref
        | "!" term "~>" type                                // perform
        | "handle" term "{" {type "~>" type "=>" term} "}"  // handle
        | term ":" type                                     // type annotation
        | "Π" term                                          // dependent product
        | "Σ" term                                          // dependent sum
        | "#" DSON term                                     // attr

[ryo33]

ありがとうございます！！！
次回はもっときれいに書くか、自分で書き起こすかするつもりです。
勝手に編集して、手書きで不満に思っていた部分などのtrivialな変更を行いました。文法は変わっていません。

[hsk]

これはDesk言語の構文ですか？

[ryo33]

はい現在の実装とは乖離がありますが定義にあわせるかたちで将来的に統一します

[hsk]

主にTAPLやCoPLなどOCaml勢の慣習にしたがって構文を書き直すと以下のように書けます:

Syntax
τ ::=                                                   type
t ::=                                                   term
    | n                                                 natural number
    | [ t1, t2, t3, ..., tn ]                           vec
    | { t11 => t12, t21 => t22, ..., tn1 => tn2 }       map
    | λ τ -> t                                          function
    | @IDENT t                                          label
    | branch t { τ11 => t12,τ21 => t22,...,τn1 => tn2 } branch
    | let t in t                                        let
    | &τ t1,t2,t3,...,tn                                ref
    | !t ~> τ                                           perform
    | handle t { τ11~>τ12=>t13, τ21~>τ22=>t23, ..., τn1~>τn2=>tn3 }
                                                        handle
    | t : τ                                             type annotation
    | @@IDENT t                                         brand
    | #DSON t                                           attr
    | <t1, t2, t3, ..., tn>                             prod
    | Π t                                               dependent product
    | Σ t                                               dependent sum

非終端記号は１文字で表し、繰り返しはt1,t2,t3,...,tnのように書いて0個からか1個からかまで厳密には表スことよりわかりやすさを優先します。term は t、type も t のように頭文字が重なってしまう場合はtype を τ のようにギリシャ文字を使うこともよくあります。

[hsk]

構文解析をすることを考えるのであればEBNFなどを使うと良いと思いますが、論文で用いられるような形式手法の形で書く場合は Rust の enum を書くようなイメージで構文を定義するのでこのような形で書くことになっていると私は思います。
構文解析も作れますけどパーサのことは考えずにASTを考えるようなつもりで書いています。

[hsk]

自分の場合はtとτがかぶるのが嫌なのでtermと考えずにexpressionと考えてtをe,τをtと書く事が多いです。
研究者によってはtermのmをとってterm を m、type を t と書くこともありけっこう自由に書いて良いものだと思うようになると思います。
Rustのenumの名前は好きにつけるのと同じです。数学的に手書きすることを考えると一文字で書くのが普通のプログラムと違うところでしょう。
名前は型も同時に表すので慣れると考えるのが楽になります。

[ryo33]

ありがとうございます！自分で使っていた形式は個人的に書きにくいのと読みづらいので慣習からあまり離れない範囲でDesk言語にあった書き方を考えてみようと思います。

[ryo33]

項::=
| λ τ → 項 (function)
| Nat
| @ Ident 項 (label)
| @@ Ident 項 (brand)

概ねこれで行こうかと

[hsk]

普通のプログラマとしては１文字で項を表すことに抵抗があるので１文字で書くなら漢字にさせてくれ。
コメントを突然書くと気持ち悪いからカッコ内にコメントを書くことにさせてくれ。みたいな気持ちなのはわかりました。

[ryo33]

実は私が書いたProductの文法には強い不満があります。ほかに良さげなものを思いつかなかったので、仮のものを書いた感じです。
現状の実装では、項と型ともに"*" "<" { term/type } ">"となっていますが、それも微妙だと思っています。
要件は

• 0-or-more な要素を含むことができる
• product/sumで相似である
• 数学的な率直であるがゆえの美しさをもつ

あたりになります。
A x B x Cのようにして別に0や⊤を作ることが一番ということは分かっているのですが、構文を過剰に減らしたいのと、ユーザーに「空のProduct」という存在を実体験してほしいため上記のような思想になっています。

[hsk]

Desk言語の実装に置いては細かい構文は重要になると思いますが、論文では主に意味論などに興味があるためproduct の機能を導入するならproduct < t1/τ1,t2/τ2,...,tn/τn > とそのまま書くほうがわかりやすいと思います。

[ryo33]

了解です。論文と実装で文法をできるだけ対応させたい思いがあったのでそのような方針になっていました。できるだけそのまま理解できるもので納得できる構文を考えてみます。

[hsk]

productの意味がよくわからないのですけどtupleな感じなのか、レコードな感じなのか、effect systemの話なのかがよくわからないので例があるとよいのではないかと思います。

[ryo33]

型を順序のない集合とした時のプロダクトになります。どう例を出していいか見当がついていません

[hsk]

なるほど、JavaやScalaでいうとSetのことですね。

[hsk]

<> + 1 = <1>
<> + 1 + 2 = <1,2>
<> + 1 + 2 + 1 = <1,2>
<> + 3 + 2 + 1 = <1,2,3>
<2,3> + <3,4> = <2,3,4>
<1,2,3> - <2,3,5> = <1>
みたいな計算ができるのではないでしょうか？

[ryo33]

はいかなり近いです。Productについては実際はkeyが型のレコードになっていて、要素が値になります。同じキーがある場合は後者の値が使われます。キーを減らす時は型強制をおこないます。
Sumについても型がタグになったタグ付きユニオンです。sakuraiさんの書かれたように同じ型があれば一つに潰れ、型強制により型レベルで要素を増やせます。項レベルではリテラルがなく、branch構文とhandle構文の評価でしか構築できません。また場合分けで要素を取り出すのはbranch構文によってのみ行えます。

[hsk]

じゃあレコードじゃないかと思いますけど

<> + <x:1> = <x:1>
<> + <x:1> + <y:2> = <x:1,y:2>
<> + <x:1> + <y:2> + <x:3> = <x:3,y:2>
<> + <z:1> + <y:2> + <x:3> = <x:3,y:2,z:1>
<x:1,y:2> + <y:3,z:4> = <x:1,y:3,z:4>
<x:1,y:2,z:3> - <y:2,z:3,a:5> = <x:1>
みたいにつかえるmapなのかな。

[ryo33]

決めました。termという概念を消します。そうすれば私がDesk言語の文法や型システムに対して抱いていた色々な不満を一挙に解決できそうです。
明日文法定義からやり直します。

[ryo33]

消すというかterm = typeにします

[hsk]

effect system の単純な実装 λeff の構文

https://github.com/Nymphium/lambdaeff/blob/master/text/main.pdf

[hsk]

色々な言語の論文の構文定義を拾ってきて見ましたが、よくあるパターンだと構文のコメントはカッコで括らなくて、１文字で非終端記号を表してます。ただカッコでコメントを書く人もいる。コメントは書かずに説明するパターンも多々ある感じです。

[ryo33]

文法を更新しました。些細なミスとかはあるかもしれませんが内容としては満足いくものになりました。
https://github.com/Hihaheho/Desk/blob/main/docs/language/formal-definition.md

[hsk]

いい感じですね。その調子で慣れていけば良いと思います。

いくつか気になった点があったので修正してみました：

tn::=                                          (number type)
    | Nat | Int | Rat | Real
    | uN | iN                                  (n-bit integer)
tt::=
    | U                                        (universe)
    | { t1, ... }                              (unordered set of types)
f ::=
    `tt` or super set of t with any t in it is replaced to `t | tn` (type family)
t ::=
    | tn
    | tn < t
    | tn < t
    | ' Char '
    | Π f
    | Σ f
    | λ t → t
    | Ident                                     (variable)
    | [ t1, ... ]                               (fixed-length vector)
    | [ t; t_len ]                              (free-length vector)
    | < t_key1 => t_value1, ... >               (map)
    | let t_def in t
    | & t t1, ...                               (application)
    | branch t { t_case1 => t1, ... }
    | ! t ~> t_out                              (perform)
    | handle t { t_in1 ~> t_out1 => t1, ... }
    | @ Ident t                                 (label)
    | @@ Ident t                                (brand)
    | t_from is t_to                            (exploit type coercion)
    | ?                                         (hole)
    | # Dson t                                  (attribute)

:== ではなく ::= にしましょう。
コメントは左揃え過右揃えにすると良いです。面倒でしょうがコメントを付けると決めたら全部つけましょう。
特に非終端記号というか型名にはコメントを付けたほうが良いと思います。

[ryo33]

:== は恥ずかしいミスでした。

コメントなのですが、self-descriptiveなものに説明がついていると自分の感覚では逆に分かりづらくなるのでこのようになっています。コメントがあったりなかったりするのが美しくないのはわかっています。self-descriptiveな構文で英語の代わりに記号を使うようにするのがいいのかもしれません。
インデントについてはあった方がいいと思っているのですが、コメントなどを揃えるのは個人的には好みではないです。vimであってもプラグインを使わないと不便ですし、モバイル端末から書いたりすることもあるので難しいと感じています。ただ、確かに読みづらいということは分かっているので何か解決方法を探してみます。mathjaxを使えば一発だと思いますが、手書きするのは苦手なのでchatgptとかにやってもらうのがいいのかもしれません。

[hsk]

コメントには説明というか名前をつけるのが普通で名前を全くつけないこともあります。
インデントを付けないで書くようなパターンを見たことはないです。
プログラミング言語でコメントを付ける場合の間隔でコメントを書きたいということでカッコをコメントにするというルールを決めたのでしょうけど、慣習的にそういった流儀で書く人は見たことがないので汚く感じます。
個人の好みでどうのという話ではないかな。
コメントを書くなら書く、書かないなら一切書かないで、説明するのが普通だと思います。

[ryo33]

確かに後から評価規則などを書くわけですしコメントなくてもいいですよね。

[hsk]

最初は練習に書いたほうがいいんじゃないかと思いますけど、量が多いから書くのがめんどくさいのでしょうｗ

[ryo33]

コンテキストも書きました。あとで追記します。

Γ :== 
| • (empty)
| Γ, a (beginning of a scope of a type variable)
| Γ, x: t (type conclusion of variable x)
| Γ, Σ f (beginning of a scope of an existential type)
| Γ, Σ f: t (type conclusion of an existential type)
| Γ, ^a (introducing of a marker)

[ryo33]

型システムの方も書き進めています。

[hsk]

まず、Σ{A,B}をΣ{C,D}のΣの意味がよくわからない状態で色々書かれても、、、。というところですのでまず構文の定義をしっかりしてから部分型付けの説明をしていただけると議論がしやすいのではないかと思います。

[hsk]

Ryoさんは https://zenn.dev/ryo33/articles/4b11a0dfede4c5 を読んで Bidirectional Type-checking を理解していることを前提で話しているようなのでその辺読んでみますね。

[ryo33]

ありがとうございます。かなり勉強になってます。taはt1~tnの一つの要素になります。
latex的にt_aと書くのがわかりやすかったかもしれません。
確かに∈を順序集合に使ってはいけないというようなルールはありませんし、Γの定義にもよるのですね。
そちらの論文だとΓ1, x, Γ2をΓ[x]と表現しているのですが意味が直感的でないと思ったのと、他の規則ではΓ1とΓ2の両方が規則中に使用されることが多いので記法に一貫性を持たせる意図がありました。

[ryo33]

ΣとΠは集合の総和と総積です。

[ryo33]

あと私が「どうですか？」的なふんわりとした質問をする時は「記法は変じゃないですか？」とか（　「なんとなく言いたいことは通じますか？」的なニュアンスです。定義が進んできて定義の詳細について議論をしたい場合は具体的な質問を行いたいと考えています。

[hsk]

型付け規則や評価規則、部分型付け規則も様々な流儀があります。

評価規則 |- e --> v

---------- (E-Int)
|- i --> i

|- e1 --> i1    |- e2 --> i2    i1 + i2 is i
-------------------------------------------- (E-Plus)
|- e1+e2 --> i

評価規則 e --> v

---------- (E-Int)
i --> i

e1 --> i1    e2 --> i2    i1 + i2 is i
-------------------------------------------- (E-Plus)
e1+e2 --> i

評価規則 {e} --> {v} (前提をifで書く)

(E-Int)     {i}     --> {i} 
(E-Plus)    {e1+e2} --> {i}   if {e1} --> {i1}, {e2} --> {i2}, i1 + i2 is i

評価規則 {e} --> {v} (前提をiffで書く)

(E-Int)     {i}     --> {i} 
(E-Plus)    {e1+e2} --> {i}   iff {e1} --> {i1}, {e2} --> {i2}, i1 + i2 is i

評価規則 e ⇓ v (前提をwhereで書く)

E-Int     i     ⇓ i 
E-Plus    e1+e2 ⇓ i   where e1 ⇓ i1, e2 ⇓ i2, i1 + i2 is i

要はわかれば良いのですが、ネストを合わせるときれいに見えます。

[ryo33]

1番上が見慣れてるのでそれで進めるつもりです。

[hsk]

Desk言語は、普通の言語からかなりかけ離れた思想で作られていると思います。
代数的効果もかなり新しい考え方ですので、詳しい説明がないとわかりません。
let式やλ抽象にしても普通は let x = 1 in x のように書いたり (λx.x+1) 3 のように使うわけですが、Deskは変数名がないので、普通ではないですよね。
その辺の説明がない状態で型付け規則を書かれてもチョットマッテとなります。

まずは構文を書いて、各要素に名前をつけそれぞれの機能についての使い方の例をあげて分かったとなった後に型付け規則などで説明してもらえるとわかりやすくなると思います。
型付け規則や、評価規則はたくさん書くことになり、それぞれの意味を説明したり証明で参照するために名前をつけると良いようです。それぞれの意味を図の説明として書くと良いと思います。

[ryo33]

ゼミで指導を受けているような感覚で私としてはすごくやりやすいのですが、sakuraiさんにとってもどかしい状態になっていないか不安です。
すべてを書ききる前に細かくフィードバックをもらったほうがいいなと個人的に思っていたので、清書することなく書いた瞬間に投稿していましたが、もしサステナブルでないのであれば、もっと大きな粒度で書き起こししたものを投稿する方向にしたほうがいいのかもしれません。

[hsk]

俺は大丈夫だけど、Ryoさんが嫌になってやめないか不安ですｗ

[hsk]

とりあえずは、構文書いて使い方の例とかを書いてドキュメント整備してから、型付け関係などのはなしに入ると良いと思います。

[ryo33]

良かったです。私は、今後も続けると思いますが、やりたくないことはやらない方針で活動しているので、虫食い算的なものが出来上がらないのか不安ではあります。

[hsk]

ま、辛いこともあるかと思いますが、できるだけ楽しくやりましょう！

[hsk]

部分型付けの規則は磯野家の例がわかりやすいですね。

:- op(500,xfx,<:).

サザエ <: 波平.
サザエ <: フネ.
カツオ <: 波平.
カツオ <: フネ.
わかめ <: 波平.
わかめ <: フネ.
タラオ <: マスオ.
タラオ <: サザエ.

t(A <: A).
t(A <: C) :- A <: B, t(B <: C).

:- t(タラオ <: タラオ).
:- t(タラオ <: サザエ).
:- t(タラオ <: 波平).
:- halt.

[hsk]

:- op(500,xfx,<:).
t(_,A <: A).
t(Γ,A <: C):- member(A<:B,Γ), t(B<:C).
t(A <: B):- t([nat <: int,int <: rat,rat <: real],A <: B).
:- t(nat <: nat).
:- t(nat <: int).
:- t(nat <: rat).
:- t(nat <: real).
:- halt.

型環境に入れておくとかすればアルゴリズミックな部分型付けの規則になる。

[ryo33]

@hsk GitHub Discussionが色々な面で不便に感じてきたのでDiscordに移行しても大丈夫ですか？

[hsk]

移動しましょうｗ
同期が取れないｗ

[ryo33]

やっぱりかなり不満に感じているのとDiscord以外を使うモチベーションがないので、移動させていただきたいです。以下が招待リンクです。
https://discord.gg/NyahPqAq9m

[hsk]

以降はdiscordを使いましょう。wikiみたいなのが欲しくなりそうな気はしますけど。