如何用"源容器"值索引"元素"类型？

Question

所以我的情况与此(非常简化)代码非常相似:

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"

我如何使用Haskell的类型系统(或GHC扩展)限制before和类似的操作Element从不同的Containers获取？我一直在研究GADTs,DataKinds但是,嗯,这需要很长时间,我可以使用一些建议或指针.(我想到的另一个想法但没有解决:使用与STmonad 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从不同的Containers中"混合" .

Answer 1

您可以通过将类型与每个容器相关联来静态地区分容器.使用类型标记容器元素以确定两个给定元素是否来自同一容器.这用-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被调用,它将产生属于同一容器的值的集合.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)