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
m...@joachim-breitner.de • http://www.joachim-breitner.de/
Jabber: nome...@joachim-breitner.de • GPG-Key: 0x4743206C
Debian Developer: nome...@debian.org
signature.asc
Description: This is a digitally signed message part
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
