Runtime "type terms" in LiquidHaskell vs. Idris

Question

I have been playing around with LiquidHaskell and Idris lately and i got a pretty specific question, that i could not find a definitive answer anywhere.

Idris is a dependently typed language which is great for the most part. However i read that some type terms during type checking can "leak" from compile-time to run-time, even tough Idris does its best to eliminate those terms (this is a special feature even..). However, this elimination is not perfect and sometimes it does happen. If, why and when this happens is not immediately clear from the code and sometimes has an effect on run-time performance.

I have seen people prefering Haskells' type system, because it cannot happen there. When type checking is done, it is done. Types are "thrown away" and not used during run-time.

What is the story for LiquidHaskell? It enhances the type system capabilities quite a bit over traditional Haskell. Does LiquidHaskell also inject run-time bits for certain type "constellations" or (as i suspect) just adds another layer of "better" types over Haskell that do not affect run-time in any shape or form.

Meaning, if one removes the special LiquidHaskell type annotations and compiles it with standard GHC, is the code produced always the same? In other words: Is the LiquidHaskell extension compile-time only?

If yes, this seems like the best of both worlds, or is LiquidHaskell just not as expressive in the type system as Idris and therefore manages without run-time terms?

Answer 1

To answer your question as asked: Liquid Haskell allows you to provide annotations that a separate tool from the compiler verifies. Code is still compiled exactly the same way.

However, I have quibbles with your question as asked. It can be argued that there are cases in which some residue of the type must survive at run time in Haskell - especially when polymorphic recursion is involved. Consider this function:

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

There is no way to statically determine the exact type involved in the use of show. Something derived from the types must survive to runtime. In practice, this is easy to do by using type class dictionaries. The theoretically important detail is that there's still type-directed behavior being chosen at runtime.