[Haskell-cafe] Re: Non-termination of type-checking
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 (c ())
unify when c = R. Although the GADTs R c below is not recursive, when
we instantiate c = R, it becomes recursive, with the negative
occurrence. The trouble is imminent.
We reach the conclusion that an instance of a non-recursive GADT
can be a recursive type. GADT may harbor recursion, so to speak.
The code below, when loaded into GHCi 6.10.4, diverges on
type-checking. It type-checks when we comment-out absurd.
{-# LANGUAGE GADTs, EmptyDataDecls #-}
data False -- No constructors
data R c where -- Not recursive
R :: (c (c ()) - False) - R (c ())
Thanks Oleg,
that's a bit simpler indeed. However, I'm skeptical on
the scoping of c here. Correct me if I'm wrong but in R's
constructor [c] is applied to () so it has to be a type
constructor variable of kind :: * - s. But [c] is also
applied to [c ()] so we must have s = * and c :: * - *.
Now given the application [R (c ())] we must have
[R :: * - *]. Then in [data R c] we must have [c :: *],
hence a contradiction?
My intuition would be that the declaration is informally
equivalent to the impredicative:
data R (c :: *) where
R :: forall c' :: * - *, (c' (c' ()) - False) - R (c' ()).
-- Matthieu___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Non-termination of type-checking
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 -XEmptyDataDecls #-}
module Impred where
The identity type
data ID a = ID a
I is from (* - *) to *, we use a partial application of [ID] here.
data I f where
I1 :: I ID
The usual reification of type equality into a term.
data Equ a b where
Eqrefl :: Equ a a
The empty type
data False
This uses impredicativity: Rdef embeds a (* - *) - *
object into R x :: *.
data R x where
Rdef :: (forall a. Equ x (I a) - a x - False) - R x
r_eqv1 :: forall p. R (I p) - p (I p) - False
r_eqv1 (Rdef f) pip = f Eqrefl pip
r_eqv2 :: forall p. (p (I p) - False) - R (I p)
r_eqv2 f = Rdef (\ eq ax -
case eq of -- Uses injectivity of type
constructors
Eqrefl - f ax)
r_eqv_not_R_1 :: R (I R) - R (I R) - False
r_eqv_not_R_1 = r_eqv1
r_eqv_not_R_2 :: (R (I R) - False) - R (I R)
r_eqv_not_R_2 = r_eqv2
rir :: R (I R)
rir = r_eqv_not_R_2 (\ rir - r_eqv_not_R_1 rir rir)
Type checking seems to loop here with ghc-6.8.3, which is a
bit strange given the simplicity of the typing problem.
Maybe it triggers a constraint with something above?
-- Loops
-- absurd :: False
-- absurd = r_eqv_not_R_1 rir rir
[1]
http://thread.gmane.org/gmane.science.mathematics.logic.coq.club/4322/focus=1405
-- Matthieu
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The container problem
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. Data.Set is a functor from the category of Haskell types *with decidable ordering* and *order-preserving* functions to itself. That's not the same category, although it is closely related. I nominate this post for the September 2008 Most Incomprehensible Cafe Post award! :-D Seriously, that sounded like gibberish. (But then, you're talking to somebody who can't figure out the difference between a set and a class, so...) All I know is that sometimes I write stuff in the list monad when the result really ought to be *sets*, not lists, because 1. there is no senamically important ordering 2. there should be no duplicates But Haskell's type system forbids me. (It also forbids me from making Set into a Functor, actually... so no fmap for you!) Think about it this way: fmap is supposed to be an homomorphism on the functor's structure, it just changes the type of the holes in the structure. To implement such map function in Set (not debating if Set should require Ord or not here!) and keep the structure invariants, the function you give to map should be order-preserving. Actually, Set.map accepts any function but it must construct the new Set using a fold behind the scenes because otherwise the function may break the internal balancing invariants. But map_monotonous is there for the case where it does respect the orders and the map can be done much more naturally and efficiently. There's simply no way to state that a function must be monotonous using haskell's limited type system. except by using a new datatype that represents only the order-preserving functions between any two types A and B (is that even possible?). So you only see the [Ord] constraint getting in the way of defining a functor on Sets, but it's more profound than that, the functions themselves don't fit exactly. Otherwise, to implement Sets correctly I think you need at least [Eq] (and give [Eq] preserving functions to fmap). You can certainly declare a new EqFunctor (f : * - *) where eqfmap : Eq a, Eq b = (a - b) - f a - f b and assume that functions are [Eq]-preserving there (similarly with [Ord]). Hope this helps, -- Matthieu___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Associative Commutative Unification
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 considering. It's quite large. The source distribution compiled effortlessly on Ubuntu. That's about all I know now. CIMe 2 is not maintained anymore, but a third version is in the works, see: http://www3.iie.cnam.fr/~urbain/a3pat/a3pat_intro.en.html -- Matthieu___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] OT - lamba calculus definition - alpha reduction
Le 29 mai 06 à 14:30, Dušan Kolář a écrit : Hello all, I'm asking in place of several my colleagues and myself of course. The question is almost off topic. It is from lambda calculus definition, in particular, definition of alpha reduction (and others as well). Alpha reduction definition: a lambda expression (\v.e) can be transformed (reduced) to (\v'.e[v'/v]) if the substitution e[v'/v] is valid. Beta reduction definition: a lambda expression (e1 e2) can be reduced to the expression e[e2/v] if e1 is of the form (\v.e) and if the substitution e[e2/v] is valid. Eta reduction definition: a lambda expression e can be reduced to a lambda expression (\v.e v) if v is not free in e. OK. If we have these two expressions: 1) (\x.x b x) 2) (\x.x c x) The question is, are they equal? (They are not identical, of course.) For answer no, there is a strong argument - there is no reduction sequence that can make these identical. On the other hand, their meaning expresses the same operation. Well, what is the answer? I will be lucky with any link to WWW resource or your opinion. Nevertheless, the more formal and precise your answer will be the more I 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___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
