Понимание приведений, используемых в шаблонах, соответствующих типу данных, который индексируется по определенному пользователю виду

Итак, я играл с DataKinds и TypeFamilies в Haskell и начал смотреть на генерируемый Core GHC.

Вот немного TestCase, чтобы мотивировать мой вопрос:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

module TestCase where

data Ty = TyBool | TyInt

type family InterpTy (t :: Ty) :: *
type instance InterpTy TyBool = Bool
type instance InterpTy TyInt  = Int

data Expr (a :: Ty) where
  I :: Int  -> Expr TyInt
  B :: Bool -> Expr TyBool

eval :: Expr a -> InterpTy a
eval (I i) = i
eval (B b) = b

Посмотрим на сгенерированное ядро для функции eval

TestCase.eval =
  \ (@ (a_aKM :: TestCase.Ty)) (ds_dL3 :: TestCase.Expr a_aKM) ->
    case ds_dL3 of _ [Occ=Dead] {
      TestCase.I dt_dLh i_as6 ->
        i_as6
        `cast` (Sub (Sym TestCase.TFCo:R:InterpTyTyInt[0])
                ; (TestCase.InterpTy (Sym dt_dLh))_R
                :: GHC.Types.Int ~# TestCase.InterpTy a_aKM);
      TestCase.B dt_dLc b_as7 ->
        b_as7
        `cast` (Sub (Sym TestCase.TFCo:R:InterpTyTyBool[0])
                ; (TestCase.InterpTy (Sym dt_dLc))_R
                :: GHC.Types.Bool ~# TestCase.InterpTy a_aKM)
    }

Очевидно, нам нужно нести информацию о том, что a может быть в конкретной ветки. Если я не индексирую Datakind и не буду использовать TypeFamilies, то это намного легче понять.

Это будет примерно так:

Main.eval =
  \ (@ a_a1hg) (ds_d1sQ :: Main.Simpl a_a1hg) ->
    case ds_d1sQ of _ [Occ=Dead] {
      Main.I' dt_d1to i_aFa ->
        i_aFa
        `cast` (Sub (Sym dt_d1to) :: GHC.Integer.Type.Integer ~# a_a1hg);
      Main.B' dt_d1tk b_aFb ->
        b_aFb `cast` (Sub (Sym dt_d1tk) :: GHC.Types.Bool ~# a_a1hg)
    }

Это я прекрасно понимаю, что меня беспокоит в примере TypeFamilies:

(Sub (Sym TestCase.TFCo:R:InterpTyTyInt[0])
      ; (TestCase.InterpTy (Sym dt_dLh))_R
      :: GHC.Types.Int ~# TestCase.InterpTy a_aKM);

Вторая строка - это то, что меня действительно смущает. Что такое точка с запятой? Кажется, это немного неуместно или я чего-то не хватает? Есть ли место, где я могу это прочитать (я с радостью беру документы, если вы можете порекомендовать его)

С уважением,

raichoo

Ответ 1

Точка с запятой - синтаксис для транзитивности принуждений.

Последний (по состоянию на сентябрь 2014 года) документ о Системе FC "Безопасные принудительные издержки в стоимости Haskell" от ICFP 2014.

В частности, на рисунке 3 этой статьи мы видим синтаксис принуждений. "γ₁; γ₂" - транзитивная транзитивность. Если γ₁ является принуждением, свидетельствующим о том, что "τ₁ ~ τ₂" и γ₂ - это принуждение, которое свидетельствует о том, что τ₂ ~ τ₃, тогда "γ₁; γ₂" является принуждением, которое свидетельствует о τ₁ ~ τ₃.

В примере, когда вы пишете eval (I i) = i то, что видит компилятор с правой стороны, это значение типа Int, и то, что ему нужно (из возвращаемого типа функции), является чем-то вроде InterpTy a, Итак, теперь нужно построить доказательство того, что Int ~ InterpTy a.

Неформально (чтение справа налево и игнорирование ролей - подробности см. в связанной статье):

Из выполнения соответствия шаблону GADT мы узнаем, что "a ~ Int" (это dt_dLh)
Поэтому мы применяем к нему Sym, чтобы получить "Int ~ a".
Затем примените семейство InterpTy, чтобы получить "InterpTy Int ~ InterpTy a" (это экземпляр/конгруэнтности/)
Затем мы составляем транзитивно с "Sym InterpTyTyInt" (это перевернутая версия аксиомы, которая гласит, что "InterpTy TyInt ~ Int" ), чтобы получить принуждение, которое мы имеем после: "Int ~ InterpTy a"