Могут ли GADT (или экзистенциалы) без ограничений быть скомпилированы так же точно, как нетипизированные обычные АТД?

Предположим, у меня есть ADT, например

data Foo = Foo !Int
         | Bar (Int->Int) Foo

Теперь скажем, я хочу наложить какую-то дополнительную безопасность типов, избавившись от «типа магического числа»:

{-# LANGUAGE GADTs #-}

newtype Intey a = Intey { getIntey :: Int }

data Foo' a where
   Foo :: !(Intey a) -> Foo' a
   Bar :: (Intey a -> Intey b) -> Foo' a -> Foo' b

Поскольку b — это просто фантомный аргумент внутри конструктора, не имеет ограничений или чего-то еще, он в основном бессмысленен — за исключением проверки типов. Поэтому может ли он скомпилироваться так же, как Foo, без каких-либо затрат на производительность и т. Д.?


performance haskell existential-type gadt
person leftaroundabout    schedule 15.04.2014    source источник
comment
Разве GADT не должны просто компилироваться в ADT + ограничения равенства, (~)s?   -  person Daniel Gratzer    schedule 15.04.2014

Ответы (1)


arrow_upward
8
arrow_downward

Вам нужно посмотреть на ядро, чтобы быть абсолютно уверенным, но в целом:

  • newtype не требует затрат времени выполнения по сравнению с базовым типом. Однако что-то вроде map getIntey по-прежнему будет проходить по списку, ничего не делая.

  • Сами типы и параметры типов стираются во время компиляции, поэтому также не должны иметь затрат во время выполнения - это одно из преимуществ статической типизации. Только если вы используете класс типа, значение времени выполнения может быть передано.

Таким образом, в большинстве случаев вы можете ожидать такой же производительности, но вам может потребоваться быть немного осторожным с операциями над контейнерами, такими как списки.

Если вы ограничитесь GHC 7.8, то новый coerce.

person GS - Apologise to Monica    schedule 15.04.2014