5

残念ながら参照が不足しているこの一節は、Haskellの歴史：クラスで怠惰であること、セクション5.1からのHaskellでのADTの開発についてです。

一般に、代数型は1つ以上の選択肢の合計を指定します。ここで、各選択肢は0個以上のフィールドの積です。完全に空のタイプであるゼロの選択肢の合計を許可することは有用だったかもしれませんが、当時、そのようなタイプの値は高く評価されていませんでした。

そのようなADTはどのように役立つのでしょうか？

4

4 に答える 4

9

理論的には、カリー・ハワード同形性は、このタイプを「誤った」命題として解釈します。「false」は、それ自体が命題として役立ちます。type Not a = a -> Falseただし、「not」コンビネータ（as ）や他の同様の構造を構築する場合にも役立ちます。

実用的に：このタイプは、パラメーター化されたデータ型の特定のブランチが存在するのを防ぐために使用できます。たとえば、ライブラリでこれを使用して、次のようなさまざまなゲームツリーを解析しました。

data RuleSet a            = Known !a | Unknown String
data GoRuleChoices        = Japanese | Chinese
data LinesOfActionChoices -- there are none in the spec!
type GoRuleSet            = RuleSet GoRuleChoices
type LinesOfActionRuleSet = RuleSet LinesOfActionChoices

これの影響は、Lines of Actionゲームツリーを解析するときに、ルールセットが指定されている場合、そのコンストラクターがであることがわかっUnknownており、パターンの一致などで他のブランチをオフのままにしておくことができることです。

于 2012-08-15T12:01:38.737 に答える
3

（別の回答で述べられているように）論理的なfalseに対応するものの中で、 GADTと組み合わせて追加の型制約を作成するためによく使用されます。例えば：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE EmptyDataDecls #-}

import Data.List (groupBy)

data Zero
data Succ n

data Vec n a where
    Nil  ::                 Vec Zero a
    Cons :: a -> Vec n a -> Vec (Succ n) a

vhead :: Vec (Succ n) a -> a
vhead (Cons v _) = v

vtail :: Vec (Succ n) a -> Vec n a
vtail (Cons _ v) = v

ここでは、コンストラクターのない2つのそのようなデータ型があります。ここでのそれらの意味は、自然数を表すことです：Zero、など。これらはデータ型のファントム型として使用されるため、その型でベクトルの長さをエンコードできます。次に、空でないベクトルにのみ適用できる/などのタイプセーフな関数を記述できます。Succ ZeroSucc (Succ Zero)Vecvheadvtail

[Haskell] Haskellの固定長ベクトル、パート1：例が詳細に説明されているGADTの使用も参照してください。

于 2012-08-15T19:06:18.657 に答える
2

コンストラクターなしのタイプの「実際の」値を作成する方法はありません（「実際の」とは、終了する計算を意味します。Haskellにはundefined :: a、error :: String -> aのような非終了のプログラムを作成する可能性がありmwahaha = mwahahaます。これを単純化すると、「」と呼びます。偽の」値）。

これがどのように役立つかの一例は、コンジットライブラリのバージョン0.5以降です。ライブラリの基本的なタイプはPipe l i o u m r;です。これらのタイプのパラメーターが異なる場合、aPipeは、ソース（入力を消費せずに出力を生成する）、シンク（出力を生成せずに入力を消費する）、またはコンジット（入力を消費して出力を生成する）のいずれかとして機能します。iとotypeパラメーターはPipe、それぞれ入力と出力のタイプです。

したがって、コンジットライブラリが、ソースの入力タイプおよびシンクの出力タイプとしてVoidfromタイプを使用することにより、ソースが入力を消費せず、シンクが出力を生成しないという概念を適用する方法の1つですData.Void。繰り返しになりますが、そのようなタイプの値を構築する終了方法はないため、シンクからの出力を消費しようとするプログラムは終了しません（これは、Haskellでは「エラーを発生させる」ことを意味し、必ずしも「永遠にループする」）。

于 2012-08-15T18:24:42.127 に答える
0

コンストラクターのない型は、ファントム型と呼ばれます。Haskellwikiのページを参照してください。

于 2012-08-15T12:16:02.560 に答える