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

Я пытаюсь составить интуитивное представление о том, когда (и сколько раз) вычисления на уровне типов с семействами типов «происходят» в 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, даже если они соответствуют одному и тому же типу. Вычисляются ли они независимо - замедляя компиляцию - или вычисление «разделяется» на уровне типа?


haskell type-level-computation type-families
person danidiaz    schedule 21.01.2019    source источник

Ответы (1)


arrow_upward
2
arrow_downward

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

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

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

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

person AntC    schedule 22.01.2019
comment
Я плохо сформулировал свой вопрос: сейчас меня интересует только производительность вычислений во время компиляции, и больше о том, сколько раз, а не когда. Я работаю над небольшой расширяемой библиотекой записей, и время компиляции для больших записей довольно велико. Немного поработав, я заметил, что иногда могу избежать дублирования вычислений, используя семейства вспомогательных типов, и это на самом деле улучшило ситуацию. Но у меня до сих пор нет хорошей мысленной модели того, как происходит компиляция, чего следует избегать и какие еще существуют средства для ускорения работы. Спасибо за указатель OutsideIn (X). - person danidiaz; 22.01.2019
comment
В качестве весьма косвенного доказательства того, что GHC в настоящее время не пытается определить два одинаковых выражения типа, см. Trac # 16070 и связанное обсуждение на github PR # 158. О том, зачем вообще задавать вопрос, когда: OutsideIn (X) имеет нечто эквивалентное (но не такое неопределенное, как) алгоритму объединения Робинсона, используемому Хиндли-Милнером; если он успешно объединяет переменную alpha с beta, считается ли это решением один или два раза? Обязательно они дубликаты (в некотором смысле). - person AntC; 23.01.2019