Безопасный API с теговыми значениями - PullRequest
Новая
       14

Безопасный API с теговыми значениями

1 голос
/ 18 мая 2019

У многих библиотек есть интерфейс, в котором необходимо сначала вызвать функцию для инициализации библиотеки, которая возвращает некоторое значение (часто указатель, иногда называемый «контекстом» или «дескриптором») для передачи другим функциям, например (в C): 

Library *initialize(long flags);
A mkA(Library *library, long n);
B mkB(Library *library, A a);

Вызов mkB, если a не был создан с тем же контекстом library - ошибка.

Я хочу связать API в Agda (через Haskell) и применить требование того же контекста в системе типов, но не уверен, как это сделать безопасно. (Обратите внимание, что API чист в том, что mkA, например, возвращает эквивалентное значение каждый раз, когда оно вызывается с одинаковыми аргументами.) Моя идея API заключается в следующем: 

module Data.Tagged where
open import Level
data Tagged {ℓ ℓ′} {A : Set ℓ} (a : A) (B : Set ℓ′) : Set (ℓ ⊔ ℓ′) where
    tag : B → Tagged a B

module Raw where
    postulate
        Library A B HsWord : Set
        initialize : IO Library
        mkA : Library → HsWord → A
        mkB : Library → A → B
    {-# COMPILE GHC Library = type Library #-}
    {-# COMPILE GHC A = type A #-}
    {-# COMPILE GHC B = type B #-}
    {-# COMPILE GHC HsWord = type Word #-}

open import Data.Tagged
open Raw public using (Library)
module _ {lib : Library} where
    A B : Set
    A = Tagged lib A
    B = Tagged lib B
    mkA : Raw.HsWord → A
    mkA n = tag (Raw.mkA lib n)
    mkB : A → B
    mkB a = tag (Raw.mkB lib a)

Таким образом, безопасность типов будет обеспечена - mkB принимает только A значения, сделанные с одинаковыми Library - за исключением того, что можно написать следующий термин: 

castTagged : ∀ {a a′ B} → Tagged a B → Tagged a′ B
castTagged (tag b) = tag b

Я бы сделал определения 

A = Tagged lib A
B = Tagged lib B

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

В любом случае, как можно определить такой безопасный для тегов API в Agda?

...