And I'm pretty sure that there's no way to convince Agda that F = R,
or something similar, because, despite the fact that Agda has
injective type constructors like GHC (R x = R y = x = y), it doesn't
let you make the inference R Unit = F Unit = R = F. Of course, in
Agda, one could arguably
We explain the technique of systematically deriving absurd terms and
apply it to type families.
Indeed I should have said that there is no _overt_ impredicative
polymorphism in the example posted earlier: it is precisely the
impredicative polymorphism that causes the paradox. As everybody
Thanks for the clear explanation, oleg.
-- ryan
On Sat, Jan 30, 2010 at 12:44 AM, o...@okmij.org wrote:
We explain the technique of systematically deriving absurd terms and
apply it to type families.
Indeed I should have said that there is no _overt_ impredicative
polymorphism in the
On Saturday 30 January 2010 3:44:35 am o...@okmij.org wrote:
It seems likely `absurd' diverges in GHCi is because of the GHC
inliner. The paper about secrets of the inliner points out that the
aggressiveness of the inliner can cause divergence in the compiler
when processing code with negative
On Friday 29 January 2010 2:56:31 am o...@okmij.org wrote:
Here is a bit more simplified version of the example. The example has
no value level recursion and no overt recursive types, and no impredicative
polymorphism. The key is the observation, made earlier, that two types
c (c ()) and
On Fri, Jan 29, 2010 at 8:56 AM, o...@okmij.org wrote:
Here is a bit more simplified version of the example. The example has
no value level recursion and no overt recursive types, and no impredicative
polymorphism. The key is the observation, made earlier, that two types
c (c ()) and
Le 29 janv. 10 à 02:56, o...@okmij.org a écrit :
Here is a bit more simplified version of the example. The example has
no value level recursion and no overt recursive types, and no
impredicative
polymorphism. The key is the observation, made earlier, that two types
c (c ()) and R
On Friday 29 January 2010 5:26:28 pm Matthieu Sozeau wrote:
data R (c :: *) where
R :: forall c' :: * - *, (c' (c' ()) - False) - R (c' ()).
This is what the data declaration is. The c on the first line and the c on the
second line are unrelated. It's sort of an oddity of GADT declarations;
Am Freitag 29 Januar 2010 23:26:28 schrieb Matthieu Sozeau:
Le 29 janv. 10 à 02:56, o...@okmij.org a écrit :
Here is a bit more simplified version of the example. The example has
no value level recursion and no overt recursive types, and no
impredicative
polymorphism. The key is the
Here is a bit more simplified version of the example. The example has
no value level recursion and no overt recursive types, and no impredicative
polymorphism. The key is the observation, made earlier, that two types
c (c ()) and R (c ())
unify when c = R. Although the GADTs R c below is
10 matches
Mail list logo
