Types are erased before run time

Question

I know for sure that in Haskell types are always erased before run-time. What happen in case of Agda?

Is dependent type information carried through to run-time ?

Answer 1

What runtime? There are at least four backends: those which target GHC (called MAlonzo), UHC, Epic and JavaScript. Some initial details can be found in the Agda wiki: you can read how the Epic backend erases types there or in this paper (the "3.3 Erasure" chapter). In short, the Epic and the UHC backends erase all types that a fully applied function receives, but doesn't perform full erasure as it can change the semantics of a program (quoted from a paper about the UHC backend):

Type translation

The remaining terms Π, Set and Level are significant for type checking only. In Agda, a value of type Set or Level cannot be inspected or pattern matched. As Agda enforces that it is impossible to observe any value of these types, they cannot affect the runtime semantics. For executing a program, it is thus safe to replace all occurrences of such values by the unit value ⊤.

One could also be tempted to completely remove any values of these kind. This could potentially alter the semantics of the translated program. Agda does not evaluate expressions under lambdas; dropping lambda abstractions taking type expressions could remove evaluation-blocking lambdas. A partial erasure of types is possible in a sound way. Saturated function applications for example can always be optimized in this way. A more detailed description of when such types may be soundly erased can be found in previous work by Letouzey.