>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 [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
