14

このプログラムに注意してください：

{-# LANGUAGE RankNTypes #-}

import Prelude hiding (sum)

type List h = forall t . (h -> t -> t) -> t -> t

sum_ :: (Num a) => List a -> a
sum_ = \ list -> list (+) 0

toList :: [a] -> List a
toList = \ list cons nil -> foldr cons nil list

sum :: (Num a) => [a] -> a
-- sum = sum_ . toList        -- does not work
sum = \ a -> sum_ (toList a)  -- works

main = print (sum [1,2,3])

合計の両方の定義は、等式の推論までは同じです。それでも、2 番目の定義のコンパイルは機能しますが、最初の定義はコンパイルされず、次のエラーが発生します。

tmpdel.hs:17:14:
    Couldn't match type ‘(a -> t0 -> t0) -> t0 -> t0’
                  with ‘forall t. (a -> t -> t) -> t -> t’
    Expected type: [a] -> List a
      Actual type: [a] -> (a -> t0 -> t0) -> t0 -> t0
    Relevant bindings include sum :: [a] -> a (bound at tmpdel.hs:17:1)
    In the second argument of ‘(.)’, namely ‘toList’
    In the expression: sum_ . toList

RankNTypes等式の推論を破るようです。それを壊すことなく、Haskellで教会でエンコードされたリストを持つ方法はありますか??

4

3 に答える 3

9

これは、あなたが試すことができるやや恐ろしいトリックです. ランク 2 の型変数を使用する場合は、代わりに空の型を使用してください。そして、型変数のインスタンス化を選択するどこでも、を使用しますunsafeCoerce。空の型を使用すると、(可能な限り) 観察できない値であるべきものを観察できるようなことをしないことが保証されます。したがって：

import Data.Void
import Unsafe.Coerce

type List a = (a -> Void -> Void) -> Void -> Void

toList :: [a] -> List a
toList xs = \cons nil -> foldr cons nil xs

sum_ :: Num a => List a -> a
sum_ xs = unsafeCoerce xs (+) 0

main :: IO ()
main = print (sum_ . toList $ [1,2,3])

次のように、少し安全なバージョンの を書きたいと思うかもしれませんunsafeCoerce:

instantiate :: List a -> (a -> r -> r) -> r -> r
instantiate = unsafeCoerce

次にsum_ xs = instantiate xs (+) 0、代替定義として問題なく機能し、自分のを本当にList a恣意的なものに変えるリスクを冒しません。

于 2015-08-11T01:30:25.533 に答える
6

一般に、等式推論は、Haskell が表す「基礎となるシステム F」でのみ成立します。この場合、他の人が指摘しているように、Haskell はforalls を左に移動し、さまざまなポイントで適切な型を自動的に適用するため、つまずきます。newtypeラッパーを介して型アプリケーションが発生する場所に関する手がかりを提供することで、これを修正できます。letHindley-Milner の型付け規則はラムダとラムダで異なるため、型の適用がeta展開によっていつ発生するかを操作することもできますforall。let名前付きバインディング) のみ。

于 2015-08-11T15:53:29.937 に答える