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?

Felucca

Note that in Idris you can annotate argument to erasure, so at least the compiler will inform you if the to-erased argument cannot be erased. Also, in Idris' successor Bloodwen: "Unbound implicit arguments are always erased, so it is a type error to attempt to pattern match on one." will be a easier to understand approach to erasure. – Sanhedrin

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.

Tort

Yes, i am aware of the second part of the answer. Type classes are Haskells method of choice for dynamic dispatch. But i think this is different in three major points. 1) It is always clear when this can potentially happen (every time one uses a type class method). 2) Often it can be optimized away (when the final type is known and specialization/inlining kicks in, the dynamic dispatch is gone). 3) This is more of a language thing in general and less of a type system thing. Even some dynamically typed languages feature dynamic dispatch... – Felucca

One thing i have to add here, is that 2) in my comment above is probably more often applicable in Haskell, then in other languages. When do we have a type where we only know that it implements 'show' but do not know the exact type. It can and does happen, but far less often than in languages like e.g. Java. But maybe i am wrong here... – Felucca