6

したがって、この（非常に単純化された）コードに非常に似た状況があります。

import Data.Maybe
import Data.List

data Container a = Container [a] 

-- Assumption: an Element can only obtained from a Container.  The operation
-- guarentees the Element is in the Container.
data Element a = Element (Container a) a

-- This operation is only valid for Elements that have the same Container.
before :: Eq a => Element a -> Element a -> Bool
before (Element (Container xs) x) (Element (Container ys) y) 
    | xs == ys = fromJust (elemIndex x xs) < fromJust (elemIndex y xs)
    | otherwise = error "Elements from different Containers"

beforeHaskell の型システム (または GHC 拡張機能) を使用して、 および類似の操作がElement異なる から を取得するのを制限するにはどうすればよいContainerですか? 私は調べていましGADTsたDataKindsが、まあ、それには長い時間がかかるので、いくつかの提案や指針を使用できます. (私が考えたがうまくいかなかった別のアイデア:STモナドのsパラメーターと同様のトリックを使用する...)

依存型言語が必要になると結論付けたら、私は悲観的すぎますか? Element依存型の型付けについての私の限られた理解が進むにつれて、型の値によって型にインデックスを付けようとしていると思うからですContainer。

編集：余分な色のために、これはすべて最終的に発生します。これは、次のようなものを非常に定義しようとしているためです。

import Data.Function
import Data.Ix

-- I want to use Elements as Array indexes; so Elements need to know
-- their Container to calculate their Int
instance Eq a => Ix (Element a) where
    -- Ignore how crap this code is
    range (l, u) = map (getSibling l) [getIndex l .. getIndex u]
    index (l,u) i = index (getIndex l, getIndex u) (getIndex i)
    inRange (l,u) i = inRange (getIndex l, getIndex u) (getIndex i)

getIndex :: Eq a => Element a -> Int
getIndex (Element (Container xs) x) = fromJust $ elemIndex x xs

getList :: Element a -> [a]
getList (Element (Container xs) _) = xs

getSibling :: Element a -> Int -> Element a
getSibling (Element (Container xs) _) i = Element (Container xs) (xs!!i)

instance Eq a => Eq (Element a) where
    (==) = (==) `on` getIndex

instance Eq a => Ord (Element a) where
    compare = compare `on` getIndex

Elementこのすべてのコードでは、異なる からのを決して「混在」させないようにする必要がありますContainer。

4

2 に答える 2

5

タイプを各コンテナに関連付けることで、コンテナを静的に区別できます。コンテナー要素は、指定された 2 つの要素が同じコンテナーに由来するかどうかを判断するためのタイプでタグ付けされます。これは-XExistentialQuantificationとを使用し-XRank2Typesます。基本的に、これは依存型指定ですが、型がコンテナー値ではなくタグに依存する点が異なります。

-- Containers with existentially typed tags 'c'
data Container a = forall c. Container !(OpenContainer c a)

-- Containers with a tag parameter 'c'
data OpenContainer c a = OpenContainer [a]

-- A container element with a tag parameter 'c'
data Element c a = Element (OpenContainer c a) a

-- Create a container.  An arbitrary tag is chosen for the container.
container :: [a] -> Container a
container = Container . OpenContainer

-- Use a container.  The tag is read.
openContainer :: Container a -> (forall c. OpenContainer c a -> b) -> b
openContainer c k = case c of Container c' -> k c'

-- Get a container's elements.  The elements are tagged.
getElements :: OpenContainer c a -> [Element c a]
getElements c@(OpenContainer xs) = map (Element c) xs

が呼び出されるたびopenContainerに、同じコンテナーに属する値のコレクションが生成されます。2 つの異なる呼び出しopenContainerは、異なるコンテナーを参照すると見なされます。

-- Ok
f c = openContainer c $ \oc -> getElements oc !! 0 `before` getElements oc !! 1

-- Error
f c d = openContainer c $ \oc -> openContainer d $ \od -> getElements oc !! 0 `before` getElements od !! 0

これは安全ですが、保守的です。これは、使用されているコンテナーではなく、使用された呼び出しに基づいているopenContainerためです。openContainerコンテナーを呼び出してから再度呼び出すと、互換性のない要素が生成されます。

-- Error
f c = openContainer c $ \oc -> openContainer c $ \od -> getElements oc !! 0 `before` getElements od !! 1

beforeこれで、等価性を明示的にテストせずに書くことができます。両方の要素のインデックスが同じであるため、同じコンテナーから取得されたものである必要があります。

before :: Eq a => Element c a -> Element c a -> Bool
before (Element (OpenContainer xs) x) (Element _ y) = fromJust (elemIndex x xs) < fromJust (elemIndex y xs)
于 2012-10-25T23:52:30.307 に答える
1

これが答えとして適格かどうかはわかりませんが、私はそれをそこに投げます。すべての要素を、それが派生するコンテナの関数にすることができます。

newtype a `HasA` b = H { using :: a -> b }
    deriving (Monad, Applicative, Functor)

許可される操作のセットを上記のクラスに制限することにより、組み合わせる要素が同じ元のコンテナーを共有するようにします。

「using」関数をエクスポートしますが、Hコンストラクターはエクスポートしません。要素を作成するプリミティブ関数はユーザーによって提供されますが、ユーザーはMonadインスタンスを使用してそれらを組み合わせることができ、コンテナーをアンラップして提供すると、常に同じコンテナーを参照するようになります。

ボーナスとして、それはあなたのタイトルの質問に文字通り答えます：それはそのコンテナの値で要素にインデックスを付けます。

于 2012-10-26T01:54:51.783 に答える