"Типовые термины" во время выполнения в LiquidHaskell vs. Idris

Question

В последнее время я играл с LiquidHaskell и Idris, и у меня возник довольно специфический вопрос, который я нигде не мог найти однозначного ответа.

Идрис - это типизированный язык, который по большей части хорош. Однако я читал, что некоторые термины типов во время проверки типов могут "просачиваться" из времени компиляции во время выполнения, даже если Idris делает все возможное, чтобы исключить эти термины (это особая функция, даже..). Тем не менее, это устранение не является совершенным, и иногда это происходит. Если, почему и когда это происходит, это не сразу понятно из кода и иногда влияет на производительность во время выполнения.

Я видел людей, предпочитающих систему типов Haskells, потому что там этого не может быть. Когда проверка типа сделана, это сделано. Типы "выбрасываются" и не используются во время выполнения.

Какова история для LiquidHaskell? Он значительно расширяет возможности системы типов по сравнению с традиционным Haskell. Вводит ли LiquidHaskell также биты времени выполнения для определенных типов "созвездий" или (как я подозреваю) просто добавляет еще один слой "лучших" типов по сравнению с Haskell, которые не влияют на время выполнения в любой форме или форме.

То есть, если кто-то удаляет специальные аннотации типа LiquidHaskell и компилирует их со стандартным GHC, всегда ли код создается одинаково? Другими словами: является ли расширение LiquidHaskell только временем компиляции?

Если да, то это кажется лучшим из обоих миров, или LiquidHaskell просто не так выразителен в системе типов, как Idris, и поэтому обходится без условий во время выполнения?

Answer 1

Чтобы ответить на ваш вопрос в виде вопроса: Liquid Haskell позволяет вам предоставлять аннотации, которые проверяет отдельный инструмент от компилятора. Код по-прежнему компилируется точно так же.

Тем не менее, у меня есть придирки с вашим вопросом, как задано Можно утверждать, что есть случаи, когда некоторые остатки типа должны выживать во время выполнения в Haskell - особенно когда задействована полиморфная рекурсия. Рассмотрим эту функцию:

lots :: Show a => Int -> a -> String
lots 0 x = show x
lots n x = lots (n-1) (x,x)

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