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
Dear Haskellers,
while trying to encode a paradox recently found in Coq if one has
impredicativity and adds injectivity of type constructors [1] I
stumbled on an apparent loop in the type checker when using GADTs,
Rank2Types and EmptyDataDecls.
{-# OPTIONS -XGADTs -XRank2Types
Le 27 sept. 08 à 15:24, Andrew Coppin a écrit :
David Menendez wrote:
I wouldn't say that. It's important to remember that Haskell class
Monad does not, and can not, represent *all* monads, only (strong)
monads built on a functor from the category of Haskell types and
functions to itself.
Le 12 juil. 08 à 04:02, John D. Ramsdell a écrit :
CIMe[1] might be useful to solve the generated diophantine equations.
It also has AC unification, and it probably wouldn't be all that hard
to translate our code into OCaml. I think CiME isn't supported
anymore. Still it's worth
will be lucky. ;-)
If b and c are free, then no, they can't be considered equal, and i
don't see how you can find a common meaning in this case either.
Those two are equivalent: (\b.\x.x b x) = (\c.\x.x c x).
-- Matthieu Sozeau
http://mattam.org___
