如何索引“元素”键入“源容器”值？ [英] How to index an "element" type by a "source container" value?

问题描述

  import Data.Maybe 
导入Data.List 
 
数据容器a =容器[a] 
 
  - 假设：元素只能从容器中获取。元素操作
  - 保留在容器中。 
数据元素a =元素（容器a）a 
 
  - 此操作仅对具有相同容器的元素有效。 
 before :: Eq a =>元素a  - >元素a  - > Bool 
 before（Element（Container xs）x）（Element（Container ys）y）
 | xs == ys = fromJust（elemIndex x xs）< fromJust（elemIndex y xs）
 |否则=错误来自不同容器的元素
  

如何使用Haskell的类型系统（或GHC扩展）限制在之前以及类似的操作从元素> Container Container C> S'我一直在寻找 GADTs 和 DataKinds ，但是，这需要很长时间，我可以使用一些建议或指针。 （我想过的另一个想法，但还没有解决：使用类似的技巧作为 ST monad的 s 参数...）

如果我认为这需要一种依赖型语言，我是否过于悲观？因为，由于我对依赖类型的理解有限，我认为我试图通过 Container 元素类型建立索引c $ c> type。

---

编辑：仅用于额外的颜色，因为我试图定义一些非常像这样的东西：
$ b $ pre $ import Data.Function
import Data.Ix

- 我想使用Elements作为数组索引;所以元素需要知道
- 他们的Container来计算他们的Int
实例Eq a => Ix（Element a）其中
- 忽略这个代码是多么垃圾
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： ：等式a =>元素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 =>等式（元素a）其中
（==）=（==）`on` getIndex

实例等式a => Ord（元素a）其中
compare = compare`on` getIndex


所有这些代码要求你永远不要混合元素 s来自不同的 Container s。

解决方案

您可以通过将类型与每个容器关联来静态地分离容器。容器元素用类型标记以确定两个给定元素是否来自同一个容器。这使用 -XExistentialQuantification 和 -XRank2Types 。基本上，这是依赖类型，除了类型取决于标签而不是容器值。

   - 存在类型的容器标签'c'
数据容器a = forall c。容器！（OpenContainer ca）
 
  - 带标签参数'c'的容器
数据OpenContainer ca = OpenContainer [a] 
 
  - 标签参数'c'
数据元素ca =元素（OpenContainer ca）a 
 
  - 创建一个容器。为容器选择一个任意标签。 
 container :: [a]  - >容器a 
容器=容器。 OpenContainer 
 
  - 使用容器。标签被读取。 
 openContainer :: Container a  - > （c。OpenContainer c a  - > b） - > b 
 openContainer c k = Container c'的情况c  - > k c'
 
  - 获取容器的元素。元素被标记。 
 getElements :: OpenContainer c a  - > [Element ca] 
 getElements c @（OpenContainer xs）= map（Element c）xs 
  

任何时候调用 openContainer ，它都会产生一组属于同一个容器的值。对 openContainer 的两个不同调用将被假定为引用不同的容器。

   -  Ok 
fc = openContainer c $ \oc  - > getElements oc !! 0`` getElements oc !! 1 
 
  - 错误
 f c d = openContainer c $ \oc  - > openContainer d $ \od  - > getElements oc !! 0```` getElements od !! 0 
  

这是安全的，但保守，因为它不是基于使用哪个容器，而是使用 openContainer 调用。在容器上调用 openContainer 然后再次调用它将产生不兼容的元素。

   - 错误
fc = openContainer c $ \oc  - > openContainer c $ \od  - > getElements oc !! 0```` getElements od !! 1 
  

现在，您可以在之前写入测试平等。由于这两个元素具有相同的索引，所以它们必须来自同一个容器。

  before :: Eq a =>元素c a  - >元素c a  - > Bool 
 before（Element（OpenContainer xs）x）（Element _y）= fromJust（elemIndex x xs）< fromJust（elemIndex y xs）
  




So I have a situation very similar to this (much simplified) code:

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"

How can I use Haskell's type system (or GHC extensions) to restrict before and similar operations from taking Elements from different Containers? I've been looking into GADTs and DataKinds but, well, that's going to take a long while and I could use some suggestions or pointers. (Another idea I've thought of but haven't worked out: use a similar trick as the ST monad's s parameter...)

Am I too pessimistic if I conclude that this would require a dependently typed language? Because, as my limited understanding of dependent typing goes, I think that I'm trying to index the Element type by values of the Container type.

---

EDIT: Just for extra color, this all ultimately arises because I'm trying to define something very much like this:

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

All of this code requires that you never "mix" Elements from different Containers.

解决方案

You can tell containers apart statically by associating a type with each container. Container elements are tagged with the type to determine whether two given elements came from the same container. This uses -XExistentialQuantification and -XRank2Types. Basically, this is dependent typing, except that types depend on the tag instead of the container value.

-- 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

Any time openContainer is called, it will yield a collection of values belonging to the same container. Two different calls to openContainer will be assumed to refer to different containers.

-- 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

This is safe, but conservative, because it is not based on which container is used, but rather which call to openContainer was used.. Calling openContainer on a container, then calling it again, will produce incompatible elements.

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

Now you can write before without explicitly testing for equality. Since both elements have the same index, they must have come from the same container.

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)

这篇关于如何索引“元素”键入“源容器”值？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！