[Haskell-cafe] Flipping *->*->* kinds, or monadic
a.biurvOir4 at asuhan.com
Sat Jul 11 06:15:53 EDT 2009
>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
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.
More information about the Haskell-Cafe