Hi, Am Dienstag, den 02.07.2013, 16:28 +0000 schrieb Simon Peyton-Jones:
| I also noticed a problem with my logic for creating the NT-lifting | function. Suppose | data C a = MkC (Foo a) | Just having the constructors of C in scope is not sufficient | to safely provide | NT a b -> NT (C a) (C b) | as the parameters of the constructor might wrap a in another type | constructor, eg | data Foo a = Foo (Set a) | | then we certainly don’t want the user to be able to write | deriving fooNT :: NT a b -> NT (Foo a) (Foo b)
Dually, suppose Foo was an *abstract* type, where we can't see the constructors of Foo. But the programmer as exported fooNT :: NT a b -> NT (Foo a) (Foo b). Then we *do* want to be able to derive cNT :: NT a b -> NT (C a) (C b) Instead maybe we say deriving cNT :: NT a b -> NT (C a) (C b) using( fooNT ) listing the imported witnesses that we use. Or maybe we say simply deriving cNT :: NT a b -> NT (C a) (C b) and magically use any NT-typed things that are in scope.
Is this really the compiler’s job here? After all, the programmer would be able to write deriving cNT' :: NT (Foo a) (Foo b) -> NT (C a) (C b) cNT :: NT a b -> NT (C a) (C b) cNT = cNT' . fooNT and expose just cNT to his users, so no expressiveness is lost by not providing automatic support here.
This clearly deserves treatment on the wiki page.
Added.
The criterion "could you write it by hand?" remains a good one.
Agreed. Greetings, Joachim -- Joachim “nomeata” Breitner mail@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nomeata@debian.org