order of arguments matters

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

order of arguments matters

Peter Padawitz
Why does only tr2 work, although the only difference between tr1 and tr2 is the order of arguments?

import Data.Tree (Tree(..))

data Type a where Tree    :: Type a -> Type (Tree a)
 Int     :: Type Int
 String  :: Type String

type Traversal1 = forall a.a -> Type a -> a

type Traversal2 = forall a.Type a -> a -> a

tr1 :: Traversal1
tr1 (Node _ (t:_)) (Tree Int) = Node 1 [t]
tr1 n Int                     = n+n
tr1 s String       = s++s

tr2 :: Traversal2
tr2 (Tree Int) (Node _ (t:_)) = Node 1 [t]
tr2 Int n                     = n+n
tr2 String s       = s++s

    Couldn't match expected type `a' against inferred type `Tree Int'
      `a' is a rigid type variable bound by
          the type signature for `tr1' at tratest.hs:9:25
    In the pattern: Node _ (t : _)
    In the definition of `tr1':
        tr1 (Node _ (t : _)) (Tree Int) = Node 1 [t]



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: order of arguments matters

Roel van Dijk-3
I believe this is caused by type equalities that are introduced by the
Type a argument. In tr2 you get something like a ~ Int or a ~ String,
allowing the function to type check. In tr1 that equality is never
introduced so the type checker thinks a and Int are distinct types.

But I'm sure someone else can provide a better (more correct) explanation.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: order of arguments matters

Roel van Dijk-3
I checked out the GHC documentation on the GADTs extension [1]:

"The key point about GADTs is that pattern matching causes type
refinement."

So in
  tr2 (Tree Int) (Node _ (t:_)) = Node 1 [t]
the 'a' in 'Type a' is refined to 'Type (Tree a)'.

But in
  tr1 (Node _ (t:_)) (Tree Int) = Node 1 [t]
you want to "generalise" the type 'Tree a' to 'Type (Tree a)', which
is not possible.


1 - http://www.haskell.org/ghc/docs/7.0-latest/html/users_guide/data-type-extensions.html#gadt

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe