Как индексировать тип элемента по значению исходного контейнера?

Итак, у меня есть ситуация, очень похожая на этот (намного упрощенный) код:

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 из разных Container? Я изучал GADTs и DataKinds, но это займет много времени, и я мог бы использовать некоторые предложения или указатели. (Еще одна идея, о которой я думал, но не реализовал: использовать аналогичный трюк, как параметр s монады ST...)

Не слишком ли я пессимистичен, если приду к выводу, что для этого потребуется язык с зависимой типизацией? Потому что, исходя из моего ограниченного понимания зависимой типизации, я думаю, что пытаюсь индексировать тип Element по значениям типа Container.

EDIT: Просто для дополнительного цвета, все это в конечном итоге возникает, потому что я пытаюсь определить что-то очень похожее на это:

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.


haskell dependent-type
person Luis Casillas    schedule 25.10.2012    source источник
comment
похоже, это связано с вопросом, можно ли определить, являются ли два значения просто равными или даже идентичными   -  person hvr    schedule 26.10.2012

Ответы (2)


arrow_upward
5
arrow_downward

Вы можете различать контейнеры статически, связывая тип с каждым контейнером. Элементы контейнера помечаются типом, чтобы определить, пришли ли два заданных элемента из одного и того же контейнера. Здесь используются -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)
person Heatsink    schedule 25.10.2012
comment
Спасибо. На самом деле я только что пробовал похожее решение только что, с RankNTypes и без экзистенциалов, но мне не пришла в голову идея промежуточного типа OpenContainer, который я включил; экземпляр Ix (Element c a) тоже работает нормально. Однако, по правде говоря, я немного надеюсь, что кто-нибудь придумает что-то, что не требует CPS, так как код становится волосатым. (Или, может быть, это мой шанс узнать ContT?) - person Luis Casillas; 26.10.2012
comment
Вам не нужно будет CPS-конвертировать ваш монадический код. Просто напишите openContainer c $ \x -> do { ... }. Это изменяет отступ, но не сантехнику монады. - person Heatsink; 27.10.2012

arrow_upward
1
arrow_downward

Я не знаю, можно ли это считать ответом, но я просто выброшу его. Вы можете сделать каждый Элемент функцией Контейнера, из которого он происходит:

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

Ограничивая набор допустимых операций указанными выше классами, вы гарантируете, что все элементы, которые вы объединяете, используют один и тот же исходный контейнер.

Вы экспортируете «использующую» функцию, но не конструктор H. Примитивные функции, которые создают элементы, предоставляются вами, но затем пользователь может просто комбинировать их с помощью экземпляра Monad, гарантируя, что они всегда будут ссылаться на один и тот же контейнер после того, как вы развернете и снабдите их контейнером.

В качестве бонуса он буквально отвечает на вопрос вашего заголовка: он индексирует элемент по значению его контейнера.

person Gabriel Gonzalez    schedule 26.10.2012
comment
Я думаю, что это предложение применимо к подобному случаю, но не совсем к тому же самому. Если я вас правильно понимаю, ваше решение требует создания Element, чтобы не потреблять Container, который будет предоставлен позже, когда будет использоваться Element. Не относится к моему случаю, но, как ни странно, я только что столкнулся с чем-то тесно связанным в моем проекте, где применима эта идея. Что забавнее, это применимо вместе с ответом Радиатора - newType SharedContainer s a = SharedContainer (OpenContainer s a -> OpenThing s a) оказывается чрезвычайно полезным экземплярам Functor и Applicative... - person Luis Casillas; 27.10.2012