Does GADTs imply ExistentialQuantification?
Hey everyone, I found that it seems that GADTs implies ExistentialQuantification, but not mentioned in the manual. Is it a bug? https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts... GHCi, version 8.4.3: http://www.haskell.org/ghc/ :? for help Prelude> :set -XGADTs -XExplicitForAll Prelude> data Q = forall a. Q a Prelude> ---- Cosmia Fu
I'm not sure. Once you have GADTs, ExistentialQuantification is just syntax. So from one angle, maybe it doesn't matter too much. On the other hand, that syntax, whole traditional, is not the clearest in the world. One could easily imagine a Haskell implementation that chooses only to support GADT syntax for existentials. So maybe it is a bug. On Aug 26, 2018 9:43 PM, "Cosmia Fu" <cosmiafu@gmail.com> wrote: Hey everyone, I found that it seems that GADTs implies ExistentialQuantification, but not mentioned in the manual. Is it a bug? https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts... GHCi, version 8.4.3: http://www.haskell.org/ghc/ :? for help Prelude> :set -XGADTs -XExplicitForAll Prelude> data Q = forall a. Q a Prelude> ---- Cosmia Fu _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
This actually looks like a bug in the implementation. If you look at the "implied flags" list for GADTs it only implies GADTSyntax and MonoLocalBinds [1]. I'm guessing that we're missing a check in the type checker code for constructors when the syntax is existential syntax (I'm not sure if we can distinguish a constructor with existential syntax vs. GADT syntax in type checker though). [1]: https://github.com/ghc/ghc/blob/c523525b0e434d848f6e47ea3f9a37485965fa79/com... Ömer David Feuer <david.feuer@gmail.com>, 27 Ağu 2018 Pzt, 04:56 tarihinde şunu yazdı:
I'm not sure. Once you have GADTs, ExistentialQuantification is just syntax. So from one angle, maybe it doesn't matter too much. On the other hand, that syntax, whole traditional, is not the clearest in the world. One could easily imagine a Haskell implementation that chooses only to support GADT syntax for existentials. So maybe it is a bug.
On Aug 26, 2018 9:43 PM, "Cosmia Fu" <cosmiafu@gmail.com> wrote:
Hey everyone,
I found that it seems that GADTs implies ExistentialQuantification, but not mentioned in the manual. Is it a bug? https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts...
GHCi, version 8.4.3: http://www.haskell.org/ghc/ :? for help Prelude> :set -XGADTs -XExplicitForAll Prelude> data Q = forall a. Q a Prelude>
----
Cosmia Fu _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
I get: Doaitse-2:~ doaitse$ ghci GHCi, version 8.4.3: http://www.haskell.org/ghc/ <http://www.haskell.org/ghc/> :? for help Prelude> :set -XGADTs Prelude> data Q = forall a.Q a <interactive>:2:10: error: Not a data constructor: ‘forall’ Perhaps you intended to use ExistentialQuantification Prelude> It is weird that the forall (which actually is an exists) was enabled by the -XExplicitForAll Doaitse
Op 27 aug. 2018, om 3:42 heeft Cosmia Fu <cosmiafu@gmail.com <mailto:cosmiafu@gmail.com>> het volgende geschreven:
Hey everyone,
I found that it seems that GADTs implies ExistentialQuantification, but not mentioned in the manual. Is it a bug? https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts... <https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-GADTs>
GHCi, version 8.4.3: http://www.haskell.org/ghc/ <http://www.haskell.org/ghc/> :? for help Prelude> :set -XGADTs -XExplicitForAll Prelude> data Q = forall a. Q a Prelude>
----
Cosmia Fu _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe <http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe> Only members subscribed via the mailman list are allowed to post.
I get: Doaitse-2:~ doaitse$ ghci GHCi, version 8.4.3: http://www.haskell.org/ghc/ <http://www.haskell.org/ghc/> :? for help Prelude> :set -XGADTs Prelude> data Q = forall a.Q a <interactive>:2:10: error: Not a data constructor: ‘forall’ Perhaps you intended to use ExistentialQuantification Prelude> It is weird that the forall (which actually is an exists) was enabled by the -XExplicitForAll Doaitse
Op 27 aug. 2018, om 3:42 heeft Cosmia Fu <cosmiafu@gmail.com <mailto:cosmiafu@gmail.com>> het volgende geschreven:
Hey everyone,
I found that it seems that GADTs implies ExistentialQuantification, but not mentioned in the manual. Is it a bug? https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts... <https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-GADTs>
GHCi, version 8.4.3: http://www.haskell.org/ghc/ <http://www.haskell.org/ghc/> :? for help Prelude> :set -XGADTs -XExplicitForAll Prelude> data Q = forall a. Q a Prelude>
----
Cosmia Fu _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe <http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe> Only members subscribed via the mailman list are allowed to post.
participants (4)
-
Cosmia Fu -
David Feuer -
Doaitse Swierstra -
Ömer Sinan Ağacan