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

Kim-Ee Yeoh 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 
>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.

More information about the Haskell-Cafe mailing list