Serge D. Mechveliani | 14 Nov 13:03 2012
Picon

local type denotation

Please,
how to correctly set an explicit type for a local value in the body of 
a polymorphic function?

Example (tested under  ghc-7.6.1):

  data D a = D1 a | D2 a (a -> a)

  f :: Eq a => D a -> a
  f (D1 x)   = x
  f (D2 x g) = let -- y :: Eq a => a
                   y = g x
               in  if x == y then x else g y

  main = putStr $ shows (f (D2 (1 :: Int) succ)) "\n"

This is compiled by    ghc --make Main

Now I need, for a certain reason, to explicitly set the type for  y  in 
`let',  with the meaning: 
"this very `a' which is in the signature for  f"
(and I think that this type Haskell assignes to  y  in  "y = g x").

I need to declare this type in a separate line:  y :: <what ever it is>.

Both  `y :: a'  and  `y :: Eq a => a'  are not compiled.

Please, copy the answer to  mechvel <at> botik.ru

Thanks,
(Continue reading)

MigMit | 14 Nov 13:24 2012
Picon

Re: local type denotation

{-# LANGUAGE ScopedTypeVariables #-}

Отправлено с iPhone

14.11.2012, в 16:03, "Serge D. Mechveliani" <mechvel <at> botik.ru> написал(а):

> Please,
> how to correctly set an explicit type for a local value in the body of 
> a polymorphic function?
> 
> Example (tested under  ghc-7.6.1):
> 
>  data D a = D1 a | D2 a (a -> a)
> 
>  f :: Eq a => D a -> a
>  f (D1 x)   = x
>  f (D2 x g) = let -- y :: Eq a => a
>                   y = g x
>               in  if x == y then x else g y
> 
>  main = putStr $ shows (f (D2 (1 :: Int) succ)) "\n"
> 
> 
> This is compiled by    ghc --make Main
> 
> Now I need, for a certain reason, to explicitly set the type for  y  in 
> `let',  with the meaning: 
> "this very `a' which is in the signature for  f"
> (and I think that this type Haskell assignes to  y  in  "y = g x").
> 
(Continue reading)

Brent Yorgey | 14 Nov 13:24 2012

Re: local type denotation

Turn on the ScopedTypeVariables extension (e.g. by putting {-#
LANGUAGE ScopedTypeVariables #-} at the top of your file), and add an
explicit 'forall a.' to the type signature of f.

-Brent

On Wed, Nov 14, 2012 at 04:03:57PM +0400, Serge D. Mechveliani wrote:
> Please,
> how to correctly set an explicit type for a local value in the body of 
> a polymorphic function?
> 
> Example (tested under  ghc-7.6.1):
> 
>   data D a = D1 a | D2 a (a -> a)
> 
>   f :: Eq a => D a -> a
>   f (D1 x)   = x
>   f (D2 x g) = let -- y :: Eq a => a
>                    y = g x
>                in  if x == y then x else g y
>                                                         
>   main = putStr $ shows (f (D2 (1 :: Int) succ)) "\n"
>                                                                
> 
> This is compiled by    ghc --make Main
> 
> Now I need, for a certain reason, to explicitly set the type for  y  in 
> `let',  with the meaning: 
> "this very `a' which is in the signature for  f"
> (and I think that this type Haskell assignes to  y  in  "y = g x").
(Continue reading)

Erik Hesselink | 14 Nov 13:25 2012
Picon

Re: local type denotation

You need to enable ScopedTypeVariables, and add a forall to introduce the type variable at the top level. The local variable will then be the *same* 'a' instead of a fresh one:

  {-# LANGUAGE ScopedTypeVariables #-}

  data D a = D1 a | D2 a (a -> a)

  f :: forall a. Eq a => D a -> a
  f (D1 x)   = x
  f (D2 x g) = let y :: Eq a => a
                   y = g x
               in  if x == y then x else g y

  main = putStr $ shows (f (D2 (1 :: Int) succ)) "\n"



On Wed, Nov 14, 2012 at 1:03 PM, Serge D. Mechveliani <mechvel <at> botik.ru> wrote:
Please,
how to correctly set an explicit type for a local value in the body of
a polymorphic function?

Example (tested under  ghc-7.6.1):

  data D a = D1 a | D2 a (a -> a)

  f :: Eq a => D a -> a
  f (D1 x)   = x
  f (D2 x g) = let -- y :: Eq a => a
                   y = g x
               in  if x == y then x else g y

  main = putStr $ shows (f (D2 (1 :: Int) succ)) "\n"


This is compiled by    ghc --make Main

Now I need, for a certain reason, to explicitly set the type for  y  in
`let',  with the meaning:
"this very `a' which is in the signature for  f"
(and I think that this type Haskell assignes to  y  in  "y = g x").

I need to declare this type in a separate line:  y :: <what ever it is>.

Both  `y :: a'  and  `y :: Eq a => a'  are not compiled.

Please, copy the answer to  mechvel <at> botik.ru

Thanks,

------
Sergei

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Richard O'Keefe | 14 Nov 23:13 2012
Picon

Re: local type denotation


On 15/11/2012, at 1:03 AM, Serge D. Mechveliani wrote:

> Please,
> how to correctly set an explicit type for a local value in the body of 
> a polymorphic function?

Other people have told you how to do it.
I'd like to tell you why you don't need to.

> 
> Example (tested under  ghc-7.6.1):
> 
>  data D a = D1 a | D2 a (a -> a)
> 
>  f :: Eq a => D a -> a
>  f (D1 x)   = x
>  f (D2 x g) = let -- y :: Eq a => a
>                   y = g x
>               in  if x == y then x else g y

You say that you want y to have exactly the type a.
Look around.  Is there some data in scope with that type?
Yes: (D2 x g) :: a => x :: a.
So you just want to say "y has the same type as x".

There's a Prelude function

	asTypeOf :: a -> a -> a
	asTypeOf x y = x

So e1 `asTypeOf` e2 gives you the value of e1,
having first ensured that e1 and e2 have the same type.

So

f :: Eq a => D a -> a
f (D1 x)   = x
f (D2 x g) = if x == y then x else g y
             where y = g x `asTypeOf` x

You apparently already know that you don't need any of this
(thanks to x == y), but want to be explicit.  The question
is how explicit you want to be.  Using asTypeOf is sort of
half way between implicit typing and showing the type you
want _as_ a type.
> 
The other question, I suppose, is _why_ you want to be explicit?

Gmane