Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 08-Oct-2021 07:00:47 JST きゅーけー

   そういえば最近 Common Lisp に静的型付け言語を埋め込むやつが話題になってたな。たしかに静的型付きでも可能ではありそう。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 08-Oct-2021 07:02:09 JST きゅーけー

     in reply to

     これだ、こうやって部分的に静的型を導入できるんだからできない理由は確かにない。

     Introducing Coalton: How to Have Our (Typed) Cake and (Safely) Eat It Too, in Common Lisp | The Coalton Languagehttps://coalton-lang.github.io/20211010-introducing-coalton/

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 08-Oct-2021 07:04:07 JST きゅーけー

     in reply to

     というかよく考えたら Typed Racket が存在するじゃん。あれも普通の Racket の世界とやりとりできるし、Typed Racket は普通にちゃんとした静的型を持った言語なのでいい。

     Guile じゃなくて Racket を導入すれば解決っぽい雰囲気あるな。まあ、Typed Racket はマクロでしっかりとした静的型を実現できることを示した例なんで、Guile でも同じことをやれば技術的に可能なことは間違いない。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 08-Oct-2021 07:06:02 JST きゅーけー

     in reply to

     あとは ACL2 みたいのを導入するとかかな。ACL2 で証明したやつを Guile に持っていきたい野望は持ってたんだけどもうほぼ挫折してる。Scheme と Common Lisp のサブセットじゃ意味論違うし。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 08-Oct-2021 07:07:21 JST きゅーけー

     in reply to

     Typed Racket は数値型が豊富で Natural 型があったりするの好き。負の数を静的に拒絶できる factorial 手続きとかが書けるので強いぞ。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 08-Oct-2021 07:08:19 JST きゅーけー

     in reply to

     まあ、今の私は ACL2 に夢中なんで ACL2 ならそれくらいのことができるのは当然なためもはやあんま嬉しくないが。