#すいません、型付きラムダ計算ってLispでできるんでしょうか？
#CommonLispそのものには型付きラムダ計算を行う機能は備わっていません。Lispで型付きラムダ計算を実装したもの、なら探せばありそうな気がします。
#単純な型付きラムダ計算じゃないですが、Schemeに型付けをできるようにしたTyped Schemeなんてのはあります。 http://www.ccs.neu.edu/home/samth/typed-scheme/ #これは通常のSchemeの上にマクロを使って実装されています。
#なるほど、実装すれば可能ということですね。ありがとうございます。
#POPL 08にHOLソース付きで出てますね(内容は新しいのかな?)。実は日曜にHOL Lightの本を衝動買いしたとこで、良い現実逃避の目標ができました :-) >Typed Schemeなんてのはあります。 http://bit.ly/19ihcZ #Typed Schemeは形だけみるとGooみたいですね('-'*)
#(df fact(n|<int> => <int>)
(cond ((= 0 n) 1)
((= 1 n) 1)
(#t (* n (fact (- n 1))))))#みたいな
#とはいえGooはDylan由来みたいですが…
COMMON LISP JP > Archives > 2009/10/28