4 ms·
AFAIK the Agda implementations use a closed universe of types and cannot be translated to an implementation of runST in Haskell which doesn't have that restrict
by cousin_it 9y ago
AFAIK the Agda implementations use a closed universe of types and cannot be translated to an implementation of runST in Haskell which doesn't have that restriction. Please correct me if I'm wrong. From a quick reading I can't tell if the new paper makes progress on that front, what do you think?