TL; DR: Я хочу реализовать объединение для полиморфизма строк, используя type family RIso (a :: [*]) (b :: [*]) :: Bool, но застрял.
Фон
Я пишу компилятор для языка с системой эффектов, которая использует полиморфизм строк, как в Расширяемые записи с метками Scoped , для представления наборов эффектов, прикрепленных к типам функций. То есть на этом языке вид стрелки функции:
(->) :: * -> * -> Effect -> *
Где Effect - это последовательность меток эффектов, таких как IO или Unsafe - либо «минусы» метки с другой строкой эффекта, переменная типа эффекта, либо «чистый» эффект (пустой строка). Простым примером является тип map:
<A, B, +E> (List<A>, (A -> B +E) -> List<B> +E)
В гипотетическом синтаксисе Haskell:
forall (a :: *) (b :: *) (e :: Effect).
(a -> Eff e b) -> [a] -> Eff e [b]
Это означает, что map принимает List значений типа A и функцию от A до B с набором эффектов +E и возвращает List из B s, также требующие эффектов +E. Чистая функция является полностью полиморфной по своему эффекту, которая по умолчанию равна пустой строке; поэтому map чисто, если его функциональный аргумент чист; в противном случае он требует тех же эффектов, что и его аргумент.
Я экспериментирую с представлением системы типов этого языка в системе типов Haskell, так что я могу опираться на проверку типов в Haskell, чтобы написать проверенную проверку типов в виде этого сообщения в блоге .
Однако, когда я приступаю к объединению типов функций, мне нужно объединить входы и выходы путем регулярного объединения (равенства), но мне нужно объединить эффекты с помощью объединения строк , которое определено так :
s ≃ { l | s′ } : θ₁
tail(r) ∉ dom(θ₁) -- †
θ₁(r) ~ θ₁(s′) : θ₂
---------------------------------------- [uni-row]
{ l | r } ~ s : θ₂ ∘ θ₁
Это говорит: «если s можно переписать в { l | s′ } при замене θ₁, а r и s′ объединить при замене θ₂, то { l | r } объединится с s при замене θ₂ ∘ θ₁, плюс боковое условие, помеченное кинжалом (†), которое я сейчас объясню.
Отношение (≃) означает, что две строки изоморфны в соответствии со следующими тремя правилами:
-------------------------- [row-head]
{ l | r } ≃ { l | r } : []
l ≠ l′
r ≃ { l | r′ } : θ
-------------------------------- [row-swap]
{ l′ | r } ≃ { l | l′ | r′ } : θ
fresh(β)
----------------------------- [row-var]
α ≃ { l | β } : [α ↦ {l | β}]
В моем текущем непроверенном проверке типов эти две функции выглядят в Haskell следующим образом:
unify typeEnv0 (Row l r) s = do
-- Attempt to rewrite.
maybeSubstitution <- isomorphicRows typeEnv0 l s (rowLast r)
case maybeSubstitution of
-- If rows are isomorphic:
Just (s', substitution, typeEnv1) -> case substitution of
-- Apply substitution, if any, and unify the tails.
Just (x, t) -> let
typeEnv2 = typeEnv1
{ typeEnvVars = Map.insert x t $ typeEnvVars typeEnv1 }
in unify typeEnv2 r s'
Nothing -> unify typeEnv1 r s'
-- Non-isomorphic rows do not unify.
Nothing -> reportTypeMismatch (Row l r) s
-- Gets the last element in a row.
rowLast :: Type -> Type
rowLast (Row _ r) = rowLast r
rowLast t = t
isomorphicRows реализует правило, описанное в статье:
Когда строка { l | r } объединяется с некоторой строкой s, мы сначала пытаемся переписать s в виде { l | s′ } […] Если это удастся, объединение продолжается объединением… хвоста строк .
Поэтому, учитывая l, r и s, вместе с правилом объединения, isomorphicRows используется, чтобы утверждать, что s может быть переписан в { l | r } при некоторой подстановке, в противном случае (Nothing) или возвращая (Just) хвост переписанной строки, подстановку (Maybe, потому что она всегда пустая или одиночная), и обновленную среду типов. На самом деле мы не передаем r, потому что нам нужен только его последний элемент rt.
isomorphicRows
:: TypeEnv -- Type environment
-> Type -- Effect label l
-> Type -- Effect row s
-> Type -- Effect row rt
-> Typecheck
(Maybe
( Type
, Maybe (TypeId, Type)
, TypeEnv
))
Правило [row-head]: строка, которая уже начинается с данной метки, тривиально переписывается заменой идентификатора.
isomorphicRows typeEnv0 l (Row l' r') _rt
| l == l'
= pure $ Just (r', Nothing, typeEnv0)
Правило [row-swap]: строка, содержащая метку где-то в ней, может быть переписана так, чтобы разместить эту метку в заголовке.
isomorphicRows typeEnv0 l (Row l' r') rt
| l /= l' = do
maybeSubstitution <- isomorphicRows typeEnv0 l r' rt
pure $ case maybeSubstitution of
Just (r'', substitution, typeEnv1) -> Just
(Row l r'', substitution, typeEnv1)
Nothing -> Nothing
Правило [row-var]: при объединении с переменной типа метка отсутствует, поэтому мы не можем напрямую проверить на равенство и должны вернуть свежую переменную для хвоста строки.
† Это обеспечивает побочное условие, которое предотвращает объединение строк с общим хвостом, но с разными префиксами, тем самым гарантируя завершение, даже если мы добавляем переменные нового типа.
isomorphicRows typeEnv0 l r@(TypeVar a) rt
| r /= rt = do
(b, typeEnv1) <- freshTypeVar typeEnv0
pure $ Just (b, Just (a, Row l b), typeEnv1)
В любом другом случае строки не изоморфны.
isomorphicRows _ _ _ _ = Nothing
Что я пытался
Я пытаюсь перевести объединение строк с помощью isomorphicRows на уровень типов, используя семейство типов, работающее со списками типов на уровне типов:
type family RIso (ra :: [*]) (rb :: [*]) :: Bool where
-- [row-head]
RIso ((l) ': r) ((l) ': s) = RIso r s
-- [row-swap]
RIso ((l) ': (l') ': r) ((l') ': (l) ': r)
= TNot (TEq l l')
RIso r r = 'True
RIso _ _ = 'False
type family TNot (a :: Bool) :: Bool where
TNot 'False = 'True
TNot 'True = 'False
type family TEq (a :: Bool) (b :: Bool) :: Bool where
TEq a a = 'True
TEq _ _ = 'False
Это похоже на основные случаи:
> :kind! RIso '[] '[]
'True
> :kind! RIso '[Int] '[Int]
'True
> :kind! RIso '[Int, Char] '[Char, Int]
'True
> :kind! RIso '[Int, Char] '[Int, String]
'False
> :kind! RIso '[Int, Char, String] '[Char, Int, String]
'True
Но не работает в более сложных случаях:
> :kind! RIso '[Int, String, Char] '[Char, Int, String]
'False
Я верю, что это потому, чтонеправильно сформулировал правило [row-swap] (TNot кажется подозрительным), и я пропускаю правило [row-var]. Я застрял в реализации [row-var], потому что я не знаю, как перенести свежую переменную типа в область видимости (или это даже правильный подход). Я попробовал это:
type family REq (ra :: [*]) (rb :: [*]) :: Bool where
…
-- [row-var]
REq (l ': r) rt = TAnd (TNot (TEq r rt)) (TEq r (Row l b))
…
type family TAnd (a :: Bool) (b :: Bool) :: Bool where
TAnd 'True 'True = 'True
TAnd _ _ = 'False
Но я не удивился, увидев, что бесплатный b генерирует ошибку типа:
error: Not in scope: type variable ‘b’
Вопрос
Можно ли ввести новую переменную с forall или чем-то, или я должен отказаться от попыток напрямую реализовать правила ввода и использовать другой подход?
В качестве альтернативы, существует ли какая-либо библиотека расширяемых записей, которая специально использует объединение строк (а не какой-либо другой метод), чтобы я мог использовать библиотеку или изучить ее технику?
Обратите внимание, что это , а не , то же самое, что простое равенство наборов, потому что могут быть повторяющиеся метки, и они «ограничены» в смысле, описанном в статье, которую я связал в верхней части этого вопроса. Это важно по двум причинам: во-первых, я собираюсь расширить это в будущем, чтобы метка эффекта могла иметь параметры типа, например, ST s; и во-вторых, я намерен использовать этот механизм для реализации расширяемых записей и вариантов на языке.