Hi again, Am Mittwoch, den 03.07.2013, 10:01 +0200 schrieb Joachim Breitner:
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.
Hmm, I notice that this is not fully thought through. A problem is that on the one hand, the operations we have on newtypes (which allow us to lift coercions between the _type_ constructor parameters) suggest that we want cNT :: NT a b -> NT (C a) (C b) while the “do it by hand” intuition suggests that cNT :: NT (Foo a) (Foo b) -> NT (C a) (C b) should be provided. But I only now notice that this function will not be easily implemented. I guess in this case it could be using NthCo to get a ~ b from Foo a ~ Foo b, but this is probably shaky. This tension between the type constructor oriented coercions and data constructor oriented policy needs a bit more thought. 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