Могат ли GADT (или екзистенциали) без ограничения да бъдат компилирани толкова плътно, колкото нетипизирани обикновени ADT?

Да предположим, че имам 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