tag:blogger.com,1999:blog-1777990983847811806.post2886506495105582920..comments2022-11-13T23:22:50.448-08:00Comments on Haskell for all: GADTsGabriella Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comBlogger8125tag:blogger.com,1999:blog-1777990983847811806.post-24449923081111259452015-09-02T04:14:16.179-07:002015-09-02T04:14:16.179-07:00Interestingly, this is really the coercion encodin...Interestingly, this is really the coercion encoding that GHC implements, only using functions to approximate coercions!<br /><br />What's wrong with the showZ function? I could write it in Agda, too. There's nothing verboten about ignoring the argument. You need to change the definition of List if you want to exclude List Int String. Taking coercions as inspiration, though, you could ask for functions *both* ways (just as coercions are invertible):<br /><br />data List a n where<br /> Nil :: (Z -> n) -> (n -> Z) -> List a n<br /> Cons :: a -> List a m -> (S m -> n) -> (n -> S m) -> List a n<br /><br />I guess List a isn't a functor anymore, though.<br /><br />Also, here's a total function from Z to S n:<br /><br />f :: Z -> S n<br />f x = case x of _ -> undefined<br /><br />The undefined there is dead code. (In GHC with EmptyCase you can just say “case x of {}”.) You don't want Z and S to be *empty* types, you want them to be *abstract* types.Luke Maurerhttps://www.blogger.com/profile/00689470087535091830noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-89299532406047724852012-06-26T11:40:25.617-07:002012-06-26T11:40:25.617-07:00Yes I have used also the free monad of coyoneda an...Yes I have used also the free monad of coyoneda and have discussed on IRC, so it is like that although I think it should be<br /><br />data FreeCoyoneda f a = Pure a | forall b. Free (f b) (b -> FreeCoyoneda f a)<br /><br />I think I am the guy who also thought of that. I have also made up things like that list with the specified number of values in the type, although I have used an uninhabited type Zero and then Maybe for the successor. You can make it like the GADT described although using this representation also means that (->) is the type of an array with the specified number of elements!Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-81734706109531027862012-06-21T17:35:44.809-07:002012-06-21T17:35:44.809-07:00Thanks. I fixed it.Thanks. I fixed it.Gabriella Gonzalezhttps://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-17365895189123698012012-06-20T04:09:34.723-07:002012-06-20T04:09:34.723-07:00There is a mistake I think:
(forall a. (a ->...There is a mistake I think:<br /> (forall a. (a -> b) -> f b) ~ f a<br /><br />'forall a' should be 'forall b'Anonymoushttps://www.blogger.com/profile/11382268504770604242noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-60095519842780441132012-06-17T12:48:39.751-07:002012-06-17T12:48:39.751-07:00Thanks. I'd always suspected they were isomor...Thanks. I'd always suspected they were isomorphic and hadn't yet proven the other direction, but your formulation makes the isomorphism clear.Gabriella Gonzalezhttps://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-90821538903087172432012-06-17T00:48:34.888-07:002012-06-17T00:48:34.888-07:00You don't need MPTCs to implement the class-ba...You don't need MPTCs to implement the class-based fake GADTs from the finally tagless paper, just classes. <br /><br />As for why quantification is enough, classes are themselves a limited form of quantification. If you attempt to desugar a typeclass into its dictionary, you'll find that almost all of them have rank 2 types.<br /><br />If you have rank 2 types, you can encode the classes from that paper as a data type, and this result should be completely unsurprising.<br /><br />As for the approach you give here, negating an existential (as you'd get from a GADT) yields the universal quantifier you see here.<br /><br />The way I've come to think of the operational monad approach vs the more direct implementation free monad or my Church encoded variant is that the operational monad is just Free (Coyoneda f), and since Coyoneda f ~ f, (modulo the extra bottom forced on you by haskell) the operational monad is isomorphic to Free f. Since Coyoneda f provides 'fmap fusion' for you, and the Free monad only uses the fmap of the underlying functor, Free (Coyoneda f) or the operational monad provide fusion for >>='s. (Also, when you fuse the Coyoneda constructor with the Free constructor from the Free monad, you can eliminate the place the extra bottom I'd mentioned hides.<br /><br />data FreeCoyoneda f a = Pure a | forall b. Free (f b) (a -> FreeCoyoneda f a)Edward Kmetthttps://www.blogger.com/profile/16144424873202502715noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-23421437800679096092012-06-16T14:06:28.604-07:002012-06-16T14:06:28.604-07:00The "datums" are the functions transform...The "datums" are the functions transforming the embedded index type (such as Z for Nil) to the exposed type (i.e. the polymorphic n). These functions are proofs that the exposed type is reachable from the embedded type (ala Curry-Howard correspondence), and every type is guaranteed to be reachable from itself via the "id", function. Therefore, at a minimum the embedded index is always reachable from itself simply by supplying "id", even if the type is completely uninhabited. However, that only works because of the lack of initiality. If Haskell somehow got rid of bottom, then yes you would need to provide a concrete constructor to define the appropriate id for that type.Gabriella Gonzalezhttps://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-20668679620694516252012-06-16T14:02:04.927-07:002012-06-16T14:02:04.927-07:00But isn't a difference between the two styles ...But isn't a difference between the two styles that in the Yoneda lemma style, you actually need a value-level datum for the list length, whereas in the GADT style this datum never has to exist at the value level?Manuel Simonihttps://www.blogger.com/profile/07840673741485280526noreply@blogger.com