Когда вычисление на уровне типов «происходит» с семействами типов? - PullRequest
Новая
       24

Когда вычисление на уровне типов «происходит» с семействами типов?

0 голосов
/ 22 января 2019

Я пытаюсь сформировать интуицию о том, когда (и сколько раз) вычисления на уровне типов с семействами типов "происходят" в Haskell. В качестве конкретного примера рассмотрим этот класс типов для индексации в n-арный продукт с использованием натурального уровня типа: 

{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies, MultiParamTypeClasses,
             ScopedTypeVariables, TypeApplications, AllowAmbiguousTypes
#-}
import Data.Kind (Type)
import Data.SOP (I(..),NP(..)) -- identity functor and n-ary product from "sop-core"

data N = Zero | Succ N -- to be used as a kind

class Key (i :: N) (ts :: [Type]) where
    type Value i ts :: Type
    getValue  :: NP I ts -> Value i ts

instance Key Zero (t:ts) where
    type Value Zero (t:ts) = t
    getValue (I v :* _) = v

instance Key n ts => Key (Succ n) (t : ts) where
    type Value (Succ n) (t:ts) = Value n ts
    getValue (_ :* rest) = getValue @n rest

getValue' :: forall n ts. Key n ts => NP I ts -> Value n ts
getValue' = getValue @n @ts

getTwoValues :: forall n ts. Key n ts => NP I ts -> NP I ts -> (Value n ts, Value n ts)
getTwoValues np1 np2 = let getty = getValue @n @ts in (getty np1, getty np2)

main :: IO ()
main = do let np = I True :* I 'c' :* Nil
          print $ getValue     @(Succ Zero) np
          print $ getValue'    @(Succ Zero) np
          print $ getTwoValues @(Succ Zero) np np

Моя интуиция заключается в том, что проверка типов при появлении getValue в main запускает «обход» списка уровня типов во время компиляции в поисках соответствующего типа значения Value (Succ Zero) '[Bool,Char]. Этот обход может быть дорогостоящим для больших списков.

А как же getValue'? Вызывает ли он «обход» списка уровней типов один раз, как прежде, или два раза, один для проверки самого getValue', а другой для проверки getValue, от которого он зависит?

А как насчет getTwoValues? В его подписи есть два вызова семейства типов Value n ts, даже если они соответствуют одному и тому же типу. Они вычисляются независимо друг от друга, что замедляет компиляцию, или вычисление «разделяется» на уровне типа?

1 Ответ

0 голосов
/ 22 января 2019

Haskell имеет "семантику стирания типа".То есть если предположить, что компилятор может разрешить все типы, тогда вывод типа «происходит» во время компиляции;во время выполнения вычислительный эффект отсутствует.

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

Документ, который объясняет вывод типов в современном GHC, в том числе для семейств типов, - это OutsideIn (X).Ваш ответ будет там.

А если серьезно, почему вы беспокоитесь о производительности внутри типа "вычисления"?Что есть, то есть.И весь ваш вопрос имеет неприятный запах ожидания процедурного алгоритма;тогда как решение типа ведет себя больше как логическое программирование.Спрашивать «когда», когда оно выполняется, еще менее уместно, чем спрашивать «когда», когда выражение вычисляется на ленивом языке.

...