On Thu, 28 Jan 2010 18:32:02 -0800, Ryan Ingram ryani.s...@gmail.com wrote:
But your example uses a recursive type; the interesting bit about this
example is that there is no recursive types or function, and yet we
can encode this loop.
The point is that you get the Fix type by (infintely)
But your example uses a recursive type; the interesting bit about this
example is that there is no recursive types or function, and yet we
can encode this loop.
-- ryan
On Wed, Jan 27, 2010 at 4:49 PM, Matthew Brecknell
matt...@brecknell.net wrote:
Ryan Ingram wrote:
The compiler doesn't
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
The compiler doesn't loop for me with GHC6.10.4; I think GADTs still
had some bugs in GHC6.8.
That said, this is pretty scary. Here's a simplified version that
shows this paradox with just a single GADT and no other extensions.
No use of fix or recursion anywhere!
{-# LANGUAGE GADTs #-}
module
Ryan Ingram wrote:
The compiler doesn't loop for me with GHC6.10.4; I think GADTs still
had some bugs in GHC6.8.
That said, this is pretty scary. Here's a simplified version that
shows this paradox with just a single GADT and no other extensions.
No use of fix or recursion anywhere!
{-#
