[Haskell-cafe] Re: Flipping *-*-* kinds, or monadic finally-tagless madness

2009-07-02 Thread Ahn, Ki Yung 

Kim-Ee Yeoh wrote:


The add function illustrates the kind of do-sugaring we know and love
that I want to use for Symantics.


   lam f   = unZ $ do
  show_c0 - get
  let
 vname = v ++ show_c0
 c0 = read show_c0 :: VarCount
 c1 = succ c0
 fz :: Z a String - Z b String
 fz = Z . f . unZ
  put (show c1)
  s - (fz . return) vname
  return $ (\\ ++ vname ++  -  ++ s ++ )


Now with lam, I get this cryptic error message (under 6.8.2):

Occurs check: cannot construct the infinite type: b = a - b
When trying to generalise the type inferred for `lam'
  Signature type: forall a1 b1.
  (Y String a1 - Y String b1) - Y String (a1 -
b1)
  Type to generalise: forall a1 b1.
  (Y String a1 - Y String b1) - Y String (a1 -
b1)
In the instance declaration for `Symantics (Y String)'

Both the two types in the error message are identical, which suggests
no generalization is needed.  I'm puzzled why ghc sees an infinite type.

Any ideas on how to proceed?


Not an answer, but just a different error message from GHC 6.10.3 when I 
  tried loading up your code.


kya...@kyavaio:~/tmp$ ghci EvalTaglessF.hs
GHCi, version 6.10.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Main ( EvalTaglessF.hs, interpreted )

EvalTaglessF.hs:264:14:
Couldn't match expected type `b1' against inferred type `b'
  `b1' is a rigid type variable bound by
   the type signature for `fz' at EvalTaglessF.hs:263:31
  `b' is a rigid type variable bound by
  the type signature for `lam' at EvalTaglessF.hs:248:26
  Expected type: Z b1 String
  Inferred type: Z b String
In the expression: Z . f . unZ
In the definition of `fz': fz = Z . f . unZ

EvalTaglessF.hs:264:22:
Couldn't match expected type `a1' against inferred type `a'
  `a1' is a rigid type variable bound by
   the type signature for `fz' at EvalTaglessF.hs:263:17
  `a' is a rigid type variable bound by
  the type signature for `lam' at EvalTaglessF.hs:248:16
  Expected type: Z a1 String
  Inferred type: Z a String
In the second argument of `(.)', namely `unZ'
In the second argument of `(.)', namely `f . unZ'
Failed, modules loaded: none.



I hope this gives you a hint, if any.  I am not exactly sure about how 
to solve this but I might try using scoped type variables extension 
somehow if I were in your shoe.


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: Flipping *-*-* kinds, or monadic finally-tagless madness

2009-07-02 Thread Edward Kmett 
Actually the problem lies in your definition of fz, it has the wrong type to
be used in lam.
The Z you get out of fz as type Z b String, but you need it to have Z (a -
b) String so that when you strip off the Z you have a Y String (a - b)
matching the result type of lam.

To get there replace your definition of fz with:

 fz :: Z a String - Z (a - b) String
 fz = Z . Y . unY . f . unZ

In 6.10.2 I used {-# LANGUAGE FlexibleInstances, TypeSynonymInstances,
MultiParamTypeClasses, ScopedTypeVariables  #-}

and that compiled just fine.

On Thu, Jul 2, 2009 at 8:02 PM, Ahn, Ki Yung kya...@gmail.com wrote:

 Kim-Ee Yeoh wrote:


 The add function illustrates the kind of do-sugaring we know and love
 that I want to use for Symantics.

lam f   = unZ $ do
  show_c0 - get
  let
 vname = v ++ show_c0
 c0 = read show_c0 :: VarCount
 c1 = succ c0
 fz :: Z a String - Z b String
 fz = Z . f . unZ
  put (show c1)
  s - (fz . return) vname
  return $ (\\ ++ vname ++  -  ++ s ++ )


 Now with lam, I get this cryptic error message (under 6.8.2):

Occurs check: cannot construct the infinite type: b = a - b
When trying to generalise the type inferred for `lam'
  Signature type: forall a1 b1.
  (Y String a1 - Y String b1) - Y String (a1 -
 b1)
  Type to generalise: forall a1 b1.
  (Y String a1 - Y String b1) - Y String (a1 -
 b1)
In the instance declaration for `Symantics (Y String)'

 Both the two types in the error message are identical, which suggests
 no generalization is needed.  I'm puzzled why ghc sees an infinite type.

 Any ideas on how to proceed?


 Not an answer, but just a different error message from GHC 6.10.3 when I
  tried loading up your code.

 kya...@kyavaio:~/tmp$ ghci EvalTaglessF.hs
 GHCi, version 6.10.3: http://www.haskell.org/ghc/  :? for help
 Loading package ghc-prim ... linking ... done.
 Loading package integer ... linking ... done.
 Loading package base ... linking ... done.
 [1 of 1] Compiling Main ( EvalTaglessF.hs, interpreted )

 EvalTaglessF.hs:264:14:
Couldn't match expected type `b1' against inferred type `b'
  `b1' is a rigid type variable bound by
   the type signature for `fz' at EvalTaglessF.hs:263:31
  `b' is a rigid type variable bound by
  the type signature for `lam' at EvalTaglessF.hs:248:26
  Expected type: Z b1 String
  Inferred type: Z b String
In the expression: Z . f . unZ
In the definition of `fz': fz = Z . f . unZ

 EvalTaglessF.hs:264:22:
Couldn't match expected type `a1' against inferred type `a'
  `a1' is a rigid type variable bound by
   the type signature for `fz' at EvalTaglessF.hs:263:17
  `a' is a rigid type variable bound by
  the type signature for `lam' at EvalTaglessF.hs:248:16
  Expected type: Z a1 String
  Inferred type: Z a String
In the second argument of `(.)', namely `unZ'
In the second argument of `(.)', namely `f . unZ'
 Failed, modules loaded: none.



 I hope this gives you a hint, if any.  I am not exactly sure about how to
 solve this but I might try using scoped type variables extension somehow if
 I were in your shoe.


 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: Flipping *-*-* kinds, or monadic finally-tagless madness

2009-07-02 Thread Ahn, Ki Yung 

Edward Kmett 쓴 글:
Actually the problem lies in your definition of fz, it has the wrong 
type to be used in lam.


The Z you get out of fz as type Z b String, but you need it to have Z (a 
- b) String so that when you strip off the Z you have a Y String (a - 
b) matching the result type of lam.


To get there replace your definition of fz with:

  fz :: Z a String - Z (a - b) String
  fz = Z . Y . unY . f . unZ


I think this seems to be the Yeoh wanted.

Mine was just blinded hack just to make it type check without looking at 
what program means.


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe