Ömer Sinan Ağacan | 5 Jul 22:35 2013
Picon

same function's type accepted in top level, but rejected in where clause

Hi all,

I came across an interesting type checker error, a function is
accepted in top level, but rejected by type checker when moved to
`where ...` clause.

I moved required code to a new module for demonstration purposes:

    module Bug where

    fix :: (a -> a) -> a
    fix f = let x = f x in x

    data Fix f = Fix (f (Fix f))

    unFix :: Fix f -> f (Fix f)
    unFix (Fix a) = a

    data ListF a l = NilF | ConsF a l

    instance Functor (ListF a) where
        fmap _ NilF        = NilF
        fmap f (ConsF a l) = ConsF a (f l)

    fold :: Functor f => (f a -> a) -> Fix f -> a
    fold f a = f (fmap (fold f) (unFix a {- f (Fix f) -}))

    unfold :: Functor f => (a -> f a) -> a -> Fix f
    unfold f a = Fix (fmap (unfold f) (f a))

(Continue reading)

David McBride | 5 Jul 22:49 2013
Picon

Re: same function's type accepted in top level, but rejected in where clause

If you remove the type signature from f in the where clause it will
work.  The reason is because the type signature listed there, the a is
a different a than in the top level signature.  If you change it from
a to x, it says it should be the a that you can't seem to specify.

If you add the pragma ScopedTypeVariables to your file, it works the
way you would assume.  However you will have to change the toplevel
signature to iterateListF :: forall a. (a -> a) -> a -> Fix (ListF a)
in order to make it work (added the forall a.).

On Fri, Jul 5, 2013 at 4:35 PM, Ömer Sinan Ağacan <omeragacan <at> gmail.com> wrote:
> Hi all,
>
> I came across an interesting type checker error, a function is
> accepted in top level, but rejected by type checker when moved to
> `where ...` clause.
>
> I moved required code to a new module for demonstration purposes:
>
>
>     module Bug where
>
>     fix :: (a -> a) -> a
>     fix f = let x = f x in x
>
>     data Fix f = Fix (f (Fix f))
>
>     unFix :: Fix f -> f (Fix f)
>     unFix (Fix a) = a
>
(Continue reading)

Ömer Sinan Ağacan | 5 Jul 23:03 2013
Picon

Re: same function's type accepted in top level, but rejected in where clause

> If you add the pragma ScopedTypeVariables to your file, it works the
> way you would assume.  However you will have to change the toplevel
> signature to iterateListF :: forall a. (a -> a) -> a -> Fix (ListF a)
> in order to make it work (added the forall a.).

Thanks, that worked.

As far as I understand, the problem is because in this definition:

    where
      f :: a -> ListF a a
      f a = ConsF a (fn a)

There's an implicit quantifier in type of `f`, like this: `f :: forall
a. a -> ListF a a`. When I add `ScopedTypeVariables` and `forall a.
...` in top level definition, it's like all `a`s in scope of top level
definition are same, except when explicitly defined as `forall a.
...`.

Is my intuition correct?

---
Ömer Sinan Ağacan
http://osa1.net
Chaddaï Fouché | 8 Jul 20:50 2013
Picon

Re: same function's type accepted in top level, but rejected in where clause

On Fri, Jul 5, 2013 at 11:03 PM, Ömer Sinan Ağacan <omeragacan <at> gmail.com> wrote:
There's an implicit quantifier in type of `f`, like this: `f :: forall
a. a -> ListF a a`. When I add `ScopedTypeVariables` and `forall a.
...` in top level definition, it's like all `a`s in scope of top level
definition are same, except when explicitly defined as `forall a.
...`.

Is my intuition correct?

Yes it is ! :)
ScopedTypeVariables is a very nice and non problematic extension, it may even be made part of some future Haskell standard.
--
Jedaï
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Mateusz Kowalczyk | 8 Jul 20:58 2013
Picon

Re: same function's type accepted in top level, but rejected in where clause


On 08/07/13 19:50, Chaddaï Fouché wrote:
> On Fri, Jul 5, 2013 at 11:03 PM, Ömer Sinan A?acan
> <omeragacan <at> gmail.com>wrote:
> 
>> There's an implicit quantifier in type of `f`, like this: `f ::
>> forall a. a -> ListF a a`. When I add `ScopedTypeVariables` and
>> `forall a. ...` in top level definition, it's like all `a`s in
>> scope of top level definition are same, except when explicitly
>> defined as `forall a. ...`.
>> 
>> Is my intuition correct?
>> 
> 
> Yes it is ! :) ScopedTypeVariables is a very nice and non
> problematic extension, it may even be made part of some future
> Haskell standard.
> 
> 
> 
> _______________________________________________ Haskell-Cafe
> mailing list Haskell-Cafe <at> haskell.org 
> http://www.haskell.org/mailman/listinfo/haskell-cafe
> 
Is this just speculation and wishful thinking or has there actually
been discussion about it already? I think it'd be great if it was the
part of the standard but I'm sure there are tens of naysayers ready to
repaint my shed.

--

-- 
Mateusz K.

Gmane