ksrky / plato Goto Github PK

現在、再帰関数は自己再帰のみしか許していない。例えば、NatやListなど。
しかし、ASTなど相互再帰が必要になることもある。
https://gitlab.haskell.org/ghc/ghc/-/blob/master/compiler/GHC/Core/TyCo/Rep.hs を見る限り、GHCは再帰型を名前的再帰で扱っているようだが、Platoでは同型再帰として扱いたい。

参考にした/なりそうなリソース

• https://ja.wikipedia.org/wiki/%E4%BB%A3%E6%95%B0%E7%9A%84%E3%83%87%E3%83%BC%E3%82%BF%E5%9E%8B
• Richard S. Bird and Lambert Meertens. Nested datatypes. In Conference on Mathematics of Program Construction, volume 1422 of LNCS, June 1998.
• Richard S. Bird and Ross Paterson. de Bruijn notation as a nested datatype. Journal of Functional Programming, To appear.](https://gitlab.haskell.org/ghc/ghc/-/blob/master/compiler/GHC/Core/TyCo/Rep.hs)

基本的には後に定義された名前が、それ以前に定義された同名の関数または型を隠すが、それらの名前の関係が対等である場合、例えば
ラムダ式の複数抽象　\x y z ...
同じスコープで定義された関数や型
における名前の衝突は検出するようにする

コンパイル時に網羅されていないパターンを検出する

現在のモジュールシステムはシステムと呼ぶに値しないような場当たり的実装になっているので、もっと形式化する。

HaskellよりMLのモジュールの方が形式的？

• F-ing Modules
• Advanced topics in types and programming languages, Chapter 8, p293

https://github.com/ksrky/lambda-calculus/tree/master/src/lambdapi