7

高階関数を使用して、型指定されていないラムダ計算でさまざまな型をエンコードできます。

Examples:
zero  = λfx.      x
one   = λfx.     fx
two   = λfx.   f(fx)
three = λfx. f(f(fx))
etc

true  = λtf. t
false = λtf. f

tuple = λxyb. b x y
null  = λp. p (λxy. false)

あまり一般的でないタイプを埋め込む研究が行われているかどうか疑問に思っていました。任意の型を埋め込むことができると主張する定理があれば素晴らしいでしょう。たとえば、kind * の型のみを埋め込むことができるなど、制限があるかもしれません。

あまり一般的ではないタイプを表現できるのであれば、例を見るのは素晴らしいことです。モナド型クラスのメンバーがどのように見えるかを特に知りたいです。

4

3 に答える 3

18

必要なほとんどすべてのタイプを表すことができます。しかし、モナド操作は型ごとに異なる方法で実装されるため、一度記述してすべてのインスタンスで機能させることはできません。>>=

ただし、型クラスのインスタンスの証拠に依存する汎用関数を作成できます。ここでは、「バインド」定義を含み、「戻り」定義を含むタプルであると考えてください。efst esnd e

bind = λe. fst e    -- after applying evidence, bind looks like λmf. ___
return = λe. snd e  -- after applying evidence, return looks like λx. ___

fst = λt. t true
snd = λt. t false

-- join x = x >>= id
join = λex. bind e x (λz. z)

-- liftM f m1 = do { x1 <- m1; return (f x1) }
-- m1 >>= \x1 -> return (f x1)
liftM = λefm. bind e m (λx. return e (f x))

次に、Monad のすべてのインスタンスに対して「証拠タプル」を定義する必要があります。bindと を定義した方法に注意してくださいreturn: これらは、定義した他の「一般的な」Monad メソッドと同じように機能します: 最初にモナド性の証拠を与えなければならず、次に期待どおりに機能します。

Maybe2 つの入力を受け取る関数として表すことができます。1 つ目は の場合に実行する関数Just xであり、2 つ目はそれが Nothing の場合に置き換える値です。

just = λxfz. f x
nothing = λfz. z

-- bind and return for maybes
bindMaybe = λmf. m f nothing
returnMaybe = just

maybeMonadEvidence = tuple bindMaybe returnMaybe

リストも同様で、折り畳み関数としてリストを表します。したがって、リストは「cons」と「empty」の 2 つの入力を受け取る関数です。次にfoldr myCons myEmpty、リストで実行します。

nil = λcz. z
cons = λhtcz. c h (t c z)

bindList = λmf. concat (map f m)
returnList = λx. cons x nil

listMonadEvidence = tuple bindList returnList

-- concat = foldr (++) []
concat = λl. l append nil

-- append xs ys = foldr (:) ys xs
append = λxy. x cons y

-- map f = foldr ((:) . f) []
map = λfl. l (λx. cons (f x)) nil

Eitherも簡単です。いずれかの型を 2 つの関数を取る関数として表します。1 つは の場合にLeft適用し、もう 1 つは の場合に適用しますRight。

left = λlfg. f l
right = λrfg. g r

-- Left l >>= f = Left l
-- Right r >>= f = f r
bindEither = λmf. m left f
returnEither = right

eitherMonadEvidence = tuple bindEither returnEither

関数自体 (a ->)がモナドを形成することを忘れないでください。そして、ラムダ計算のすべては関数です...だから...あまり難しく考えないでください。;) Control.Monad.Instancesのソースから直接インスピレーションを得ています

-- f >>= k = \ r -> k (f r) r
bindFunc = λfkr. k (f r) r
-- return = const
returnFunc = λxy. x

funcMonadEvidence = tuple bindFunc returnFunc
于 2012-01-20T02:50:47.747 に答える
12

タイプレベルと値レベルを混同しています。型指定されていないラムダ計算には、モナドはありません。モナド操作（値レベル）はありますが、モナド（タイプレベル）はありません。ただし、操作自体は同じであるため、表現力を失うことはありません。したがって、質問自体は実際には意味がありません。

于 2012-01-19T11:24:57.730 に答える
1

さて、すでにタプルとブール値があるので、それにEither基づいて非再帰的な合計型を表すことができます。

type Either a b = (Bool, (a, b))
type Maybe a    = Either () a

そして Maybe は Monad 型クラスのメンバーです。ラムダ表記への変換は演習として残します。

于 2012-01-19T11:33:20.890 に答える