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

2009-07-11 Thread Kim-Ee Yeoh 

Kim-Ee Yeoh wrote:
 As for fixing the original bug, I've found that the real magic lies
 in the incantation (Y . unY) inserted at the appropriate places.

Aka unsafeCoerce, changing the phantom type |a|.

The type of (Y . unY) is 

(Y . unY) :: forall a b c. Y c a - Y c b

so modulo (Y c), it is indeed unsafeCoerce.

The need to do it is caused by wanting to erase the existential introduced 
by Za/MkZa. 

That's not the primary reason. The earlier version of the code
in my original message doesn't use existentials. We still however,
need to wobble the type via (Y . unY) in order to typecheck.

Depending on what the phantom type is supposed to represent, this may or 
may not give the semantics/safety you're after.

If you're referring to the safety of the object/target language, then even
without any Symantics instances, only type-correct code can compile,
thanks to the finally-tagless embedding that lifts type-checking in
the meta-language (Haskell) into type-checking for the target language.

That safety isn't in the least bit compromised.

The pretty-printing Symantics instance in question actually 
type-checks fine without unsafeCoerce or its like when written out
without the additional Monad type-class abstraction and Y-Z 
isomorphism. Translating to the latter was entirely straightforward.

Thanks to all who responded.

-- 
View this message in context: 
http://www.nabble.com/Flipping-*-%3E*-%3E*-kinds%2C-or-monadic-finally-tagless-madness-tp24314553p24439023.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

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

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

2009-07-03 Thread Kim-Ee Yeoh 

Hi Edward,

Your runPretty version fits the bill nicely, thank you. I might still retain
the state monad version because it allows generalizations beyond
pretty-printing.

As for fixing the original bug, I've found that the real magic lies
in the incantation (Y . unY) inserted at the appropriate places. Indeed,
I've removed type signatures because try as I might, I couldn't
write something the type-checker would accept. This is for 6.8.2.

FWIW, the final version:

instance Symantics (Y String)  where
int   = unZ . return . show
bool  = unZ . return . show
lam f  = unZ $ do
   show_c0 - get
   let
  vname = v ++ show_c0
  c0 = read show_c0 :: VarCount
  c1 = succ c0
   put (show c1)
   bodyf - (Z . Y . unY . f . unZ . return) vname
   return $ (\\ ++ vname ++  -  ++ bodyf ++ )
fix f= pr3 [MkZa $ lam f] [(fix , )]
app e1 e2= pr3 [MkZa e1,MkZa e2] [(,,)]
add e1 e2= pr3 [MkZa e1,MkZa e2] [(, +  ,)]
mul e1 e2= pr3 [MkZa e1,MkZa e2] [(, *  ,)]
leq e1 e2= pr3 [MkZa e1,MkZa e2] [(, = ,)]
if_ be et ee = pr3 [MkZa be,MkZa et,MkZa ee] [(if , then , else
,)]

-- Suppress the Symantics phantom type by casting to an existential
data Za  where
MkZa :: Y String a - Za

pr3 a b = unZ $ pr2 a b

pr2 :: forall a. [Za] - [String] - Z a String
pr2 _  [] = return 
pr2 [] ts = (return . concat) ts
pr2 ((MkZa e):es) (t:ts) = do
s1 - (Z . Y . unY) e   -- that (Y . unY) magical
incantation again!
s2 - pr2 es ts
return $ t ++ s1 ++ s2



Edward Kmett wrote:
 
 You might also look at doing it without all the State monad noise with
 something like:
 class Symantics repr  where
int :: Int  - repr Int
add :: repr Int  - repr Int - repr Int
lam :: (repr a - repr b) - repr (a-b)
app :: repr (a - b) - repr a - repr b
 
 newtype Pretty a = Pretty { runPretty :: [String] - String }
 
 pretty :: Pretty a - String
 pretty (Pretty f) = f vars where
 vars = [ [i] | i - ['a'..'z']] ++ [i : show j | j - [1..], i -
 ['a'..'z'] ]
 
 instance Symantics Pretty where
int = Pretty . const . show
add x y = Pretty $ \vars - ( ++ runPretty x vars ++  +  ++
 runPretty y vars ++ )
lam f = Pretty $ \ (v:vars) - (\\ ++ v ++ .  ++ runPretty (f (var
 v)) vars ++ ) where
var = Pretty . const
app f x = Pretty $ \vars - ( ++ runPretty f vars ++   ++
 runPretty
 x vars ++ )
 

-- 
View this message in context: 
http://www.nabble.com/Flipping-*-%3E*-%3E*-kinds%2C-or-monadic-finally-tagless-madness-tp24314553p24326046.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

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

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

2009-07-03 Thread wren ng thornton 

Kim-Ee Yeoh wrote:
  type VarCount = int
  newtype Y b a = Y {unY :: VarCount - (b, VarCount)}


Hi Edward,

Your runPretty version fits the bill nicely, thank you. I might still retain
the state monad version because it allows generalizations beyond
pretty-printing.

As for fixing the original bug, I've found that the real magic lies
in the incantation (Y . unY) inserted at the appropriate places.


Aka unsafeCoerce, changing the phantom type |a|. The need to do it is 
caused by wanting to erase the existential introduced by Za/MkZa. 
Depending on what the phantom type is supposed to represent, this may or 
may not give the semantics/safety you're after.


--
Live well,
~wren
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

2009-07-02 Thread Kim-Ee Yeoh 

I'm trying to write HOAS Show instances for the finally-tagless
type-classes using actual State monads.  

The original code:
http://okmij.org/ftp/Computation/FLOLAC/EvalTaglessF.hs

Two type variables are needed: one to vary over the Symantics 
class (but only as a phantom type) and another to vary over the 
Monad class. Hence, the use of 2-variable type constructors.

 type VarCount = int
 newtype Y b a = Y {unY :: VarCount - (b, VarCount)}

Not knowing of a type-level 'flip', I resort to newtype isomorphisms:

 newtype Z a b = Z {unZ :: Y b a}
 instance Monad (Z a)  where
return x = Z $ Y $ \c  - (x,c)
(Z (Y m)) = f  = Z $ Y $ \c0 - let (x,c1) = m c0 in (unY . unZ) (f
 x) c1-- Pace, too-strict puritans
 instance MonadState String (Z a)  where
get   = Z $ Y $ \c - (show c, c)
put x = Z $ Y $ \_ - ((), read x)

So far so good.  Now for the Symantics instances (abridged).

 class Symantics repr  where
int  :: Int  - repr Int  -- int literal
add :: repr Int  - repr Int - repr Int
lam :: (repr a - repr b) - repr (a-b)

 instance Symantics (Y String)  where
int = unZ . return . show
add x y = unZ $ do
   sx - Z x
   sy - Z y
   return $ ( ++ sx ++  +  ++ sy ++ )

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?

-- 
View this message in context: 
http://www.nabble.com/Flipping-*-%3E*-%3E*-kinds%2C-or-monadic-finally-tagless-madness-tp24314553p24314553.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

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

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

2009-07-02 Thread Edward Kmett 
You might also look at doing it without all the State monad noise with
something like:
 class Symantics repr  where
int :: Int  - repr Int
add :: repr Int  - repr Int - repr Int
lam :: (repr a - repr b) - repr (a-b)
app :: repr (a - b) - repr a - repr b

 newtype Pretty a = Pretty { runPretty :: [String] - String }

 pretty :: Pretty a - String
 pretty (Pretty f) = f vars where
 vars = [ [i] | i - ['a'..'z']] ++ [i : show j | j - [1..], i -
['a'..'z'] ]

 instance Symantics Pretty where
int = Pretty . const . show
add x y = Pretty $ \vars - ( ++ runPretty x vars ++  +  ++
runPretty y vars ++ )
lam f = Pretty $ \ (v:vars) - (\\ ++ v ++ .  ++ runPretty (f (var
v)) vars ++ ) where
var = Pretty . const
app f x = Pretty $ \vars - ( ++ runPretty f vars ++   ++ runPretty
x vars ++ )

-Edward Kmett

On Thu, Jul 2, 2009 at 5:52 PM, Kim-Ee Yeoh a.biurvo...@asuhan.com wrote:


 I'm trying to write HOAS Show instances for the finally-tagless
 type-classes using actual State monads.

 The original code:
 http://okmij.org/ftp/Computation/FLOLAC/EvalTaglessF.hs

 Two type variables are needed: one to vary over the Symantics
 class (but only as a phantom type) and another to vary over the
 Monad class. Hence, the use of 2-variable type constructors.

  type VarCount = int
  newtype Y b a = Y {unY :: VarCount - (b, VarCount)}

 Not knowing of a type-level 'flip', I resort to newtype isomorphisms:

  newtype Z a b = Z {unZ :: Y b a}
  instance Monad (Z a)  where
 return x = Z $ Y $ \c  - (x,c)
 (Z (Y m)) = f  = Z $ Y $ \c0 - let (x,c1) = m c0 in (unY . unZ) (f
  x) c1-- Pace, too-strict puritans
  instance MonadState String (Z a)  where
 get   = Z $ Y $ \c - (show c, c)
 put x = Z $ Y $ \_ - ((), read x)

 So far so good.  Now for the Symantics instances (abridged).

  class Symantics repr  where
 int  :: Int  - repr Int  -- int literal
 add :: repr Int  - repr Int - repr Int
 lam :: (repr a - repr b) - repr (a-b)

  instance Symantics (Y String)  where
 int = unZ . return . show
 add x y = unZ $ do
sx - Z x
sy - Z y
return $ ( ++ sx ++  +  ++ sy ++ )

 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?

 --
 View this message in context:
 http://www.nabble.com/Flipping-*-%3E*-%3E*-kinds%2C-or-monadic-finally-tagless-madness-tp24314553p24314553.html
 Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

 ___
 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