[Agda] strictness switch

Nils Anders Danielsson nad at cse.gu.se
Wed Feb 1 15:32:43 CET 2017


On 2017-01-20 11:35, Sergei Meshveliani wrote:
> Is it possible to switch on strictness for the Agda type checker?
> How much of strictness can be switched on?
> It is interesting to see how does strictness effect on the type check
> cost for a particular example.

Just for fun I tried to compile Agda using -XStrict, but unfortunately
GHC panicked. Even if the compilation had succeeded I expect that Agda
wouldn't have become faster: it might have looped, or forced thunks that
do not need to be forced.

-- 
/NAD


More information about the Agda mailing list