Make symbols for type constructors

[goldfirere]

If I say

$(singletons [d|
  data Either a b = Left a | Right b
  |])

then I expect to have EitherSym0 :: TyFun * (TyFun * * -> *) -> *

[goldfirere]

Ditto for $(genDefunSymbols [''Either]).

[jstolarek]

That should be simple, but what is the purpose?

Left is a data constructor, LeftSym0 is a type-level symbol for promoted Left, Either is a type constructor. What will EitherSym0 be? A kind-level symbol for promoted Either? Can we wish to partially apply Either using symbols? That's something we cannot do normally. Sorry if these questions don't make sense but I'm lost here.

[goldfirere]

I wanted to say, in hand-written code, ZipWith EitherSym0 '[Int, Bool] '[Char, Double] and get '[Either Int Char, Either Bool Double].

[jstolarek]

Hm... this does not have term-level equivalent, right?

[goldfirere]

We could say that (typeRep :: Proxy Either) should promote to EitherSym0, but that's a story for another day. So, I would say the answer is "Agreed, this does not have a term-level equivalent."

On Mar 21, 2014, at 10:04 AM, Jan Stolarek wrote:

Hm... this does not have term-level equivalent, right?

— Reply to this email directly or view it on GitHub.

[jstolarek]

I just spent almost three hours on this one, which is very annoying because this is almost a one-line fix. The only theoretical problem are data types that have same names of type and value constructor, because names of generated symbol are identical. This however is easy to fix.

But I've ran into a problem with empty tuples that I just can't fix. In general tuples and lists are a special case of data types that have identical type and value constructors. To deal with this I generate symbols like TyCtorTuple2Sym0 for type constructors (for data constructor the symbol is Tuple2Sym0). There is a small problem when generating instances of Apply, because the last instance refers to non-existing type:

type instance Apply (TyCtorTuple2Sym1 a) b = TyCtorTuple2 a b
type instance Apply TyCtorTuple2Sym0 a = TyCtorTuple2Sym1 a

To solve this I generate a type synonym:

type TyCtorTuple2 = (,)

However, this does not work for empty tuples. Calling genSingletons on ''() causes this error:

Splices.hs:76:3: Not in scope: data constructor ‘TyCtorTuple0’

This is true - there is no data constructor names TyCtorTuple0. But the problem is that such constructor should never be mentioned. After commenting out all references to () in singletons I was able to compile the library and call $(genSingletons [ ''() ]) from another file. The result looks like this:

    type TyCtorTuple0 = GHC.Tuple.()
    type TyCtorTuple0Sym0 = TyCtorTuple0
    type Tuple0Sym0 = GHC.Tuple.()
    data instance Sing (z_a4dQ :: GHC.Tuple.())
      = z_a4dQ ~ GHC.Tuple.() => STuple0
    type STuple0 (z_a4dQ :: GHC.Tuple.()) = Sing z_a4dQ
    instance SingKind (KProxy :: KProxy GHC.Tuple.()) where
      type DemoteRep (KProxy :: KProxy GHC.Tuple.()) = GHC.Tuple.()
      fromSing STuple0 = GHC.Tuple.()
      toSing GHC.Tuple.() = SomeSing STuple0
    instance SingI GHC.Tuple.() where
      sing = STuple0

Splices.hs:76:3: Not in scope: data constructor ‘TyCtorTuple0’

I don't see TyCtorTuple0 data constructor here, just type constructor. I have no idea what's going on here, especially that these declarations work perfectly fine when simply placed in a file. Help? The relevant code is here: https://github.com/goldfirere/singletons/blob/0bd945c6dad2e36aa01ee09236bee52cccd74e0b/src/Data/Singletons/Promote.hs#L538

[goldfirere]

Yuck.

I think the problem is simple: it's the use of PromotedT in buildEmptySymDec. PromotedT causes a lookup in the data constructor namespace. ConT, on the other hand, looks up in the type constructor namespace, and then tries the data constructor namespace if the first lookup fails. (It's parallel to the behavior of Foo vs. 'Foo in normal code.) What further confuses all of this is that some Names have their namespace baked in (in which case PromotedT and ConT are completely synonymous).

The correct solution here, I believe, is to enhance mkName to take a namespace. Then, we will never have to worry about the ConT / PromotedT distinction. (mkName creates a name without a baked-in namespace.) It may be possible to make this glorified mkName without changing GHC. I'll see if I can put it in the th-desugar library, as the feature is likely useful to others as well.

In thinking about this, I came up with a much simpler solution all around, for this particular problem: just say type EitherSym0 = TyCon2 Either, for the as-yet-undefined TyCon2. We could also produce type EitherSym1 a = TyCon1 (Either a). Oh, I suppose those need to be TyCtorEitherSym0 and TyCtorEitherSym1. Bah.

[jstolarek]

The correct solution here, I believe, is to enhance mkName to take a namespace.

I decided to go with the simplest solution and changed PromotedT to ConT in buildEmptySymDec. That seems to work perfectly fine.

In thinking about this, I came up with a much simpler solution all around, for this particular problem: just say type EitherSym0 = TyCon2 Either, for the as-yet-undefined TyCon2. We could also produce type EitherSym1 a = TyCon1 (Either a).

I'm not sure if this is simpler, at least in terms of implementation work. With my current approach we are reusing infrastructure for data constructor symbol generation. What you propose requires writing some code specialy to deal with type constructors.

type EitherSym1 a = TyCon1 (Either a)

Hm... up till now I was convinced that you can't say 'Either a`. Aren't type constructors supposed to be saturated?

[jstolarek]

I'm marking this as fixed. If you think this can be implemented better please reopen.

[goldfirere]

No, type constructors don't need to be saturated, just type functions. Unsaturated type constructors come up fairly often, such as in any Monad instance.

As for the PromotedT --> ConT solution, it makes me worried. Sometimes, the name you are using there is the name of a promoted data constructor, where PromotedT is more appropriate. As it happens, it seems we have Names with baked-in namespaces, so this solution works. But, if somehow we were to use naked Names (created from mkName, perhaps), then this would unexpectedly break. Really, we should have some logic here to decide between ConT and PromotedT, or more reliable namespaces.

I'm happy to take a closer look soon.

[jstolarek]

No, type constructors don't need to be saturated, just type functions.

Right. I got confused because of "Associated types with class" paper where it says: wherever the type constructor appears, it must be applied to at least as many type arguments as there are class parameters. I somehow generalized this to any usage of type constructor.

As for the PromotedT --> ConT solution, it makes me worried.

I'll put a short comment in the source code so we don't forget that.

[goldfirere]

In thinking more about this, I favor removing this implementation. Why? The chief reason is that it's wrong: most data definitions don't use kind signatures, and the defunctionalized symbol generation will get its kinds wrong if there is a type parameter of a kind other than *. (See this line -- it assumes all tyvars have kind *.)

Could this be fixed? I suppose, by being poly-kinded for all unannotated tyvars.

The other annoying problem here is naming. The current scheme for name promotion will fail on symbolic names (like data a + b = ..., which is legal). Of course this can be solved, but I think we're blowing our complexity budget. Given how easy it is for users to say TyCon2 Either, this seems like more trouble that it's worth.

[jstolarek]

After looking at the code I think that fixing current implementation should be simple.

being poly-kinded for all unannotated tyvars.

That's simple - we can easily recover existing kind variables, generate new ones for PlainTV and pass them to buildCtorSyms instead of list of StarTs.

The other annoying problem here is naming.

This will require one more guard in tyCtorName. That's not technically difficult although we will have to come up with a naming convention for infix type constructor symbols and I agree this gets a bit annoying.

[jstolarek]

After a few experiments I am not convinced that you're right. I remember that poly-kinded things don't promote. Now I discovered that when I write:

data Either a b = Left a | Right b

then a and b are inferred to have kind * because they are used as parameters for at least one data constructor and the datatype promotes (I am assuming here PolyKinds and DataKinds + KindSignatures obviously). So a datatype like this will not promote:

data Either a b = Left a | Right

It requires b :: * kind signature to promote. Therefore, since poly-kinded datatypes don't promote it is right to assume * as kinds of type variables. Am I missing something here?

But I discovered another problem. We generate symbols for promoted datatype even if that datatype is not promotable. This does not make sense and leads to compilation error:

data Either a b = Left a | Right

Splices.hs:(39,3)-(41,3)
    data Either_a2NA a_a2NE (b_a2NF :: k_a2ND)
      = Left_a2NC a_a2NE | Right_a2NB
    data LeftSym0 (k_a2NG :: TyFun a_a2NE (Either_a2NA a_a2NE b_a2NF))
    type instance Apply LeftSym0 a_a2NH = Left_a2NC a_a2NH
    type RightSym0 = Right_a2NB

Splices.hs:39:3:
    Data constructor ‘Right’ comes from an un-promotable type ‘Either’
    In the type ‘Right’
    In the type declaration for ‘RightSym0’

Can/Should we get this one right?

[jstolarek]

After some more thought I see it is correct to have type constructor symbols for non-promotable datatypes. But the datatype must be a phantom type, so I'm not sure how useful is that (aside from Proxy).

[goldfirere]

Or it could be something like data X a b = MkX (a b). Here, even without PolyKinds, we get that a :: * -> *. (With PolyKinds, it's a :: k -> *.)

As to your earlier question about getting it right: I think the answer is "no". If a user tries to promote something that Haskell doesn't support promotion for, then that's their problem. This is definitely a limitation we have to mention in the paper.

I can imagine a fair amount more work being done to detect cases where GHC doesn't support the promotion, so neither do we. If we detect these cases, we could produce better error messages. But, that's bottom priority for me, at this point.

[jstolarek]

If a user tries to promote something that Haskell doesn't support promotion for, then that's their problem.

Right. What about this:

since poly-kinded datatypes don't promote it is right to assume * as kinds of type variables.

If I'm right about this do we need to change anything in existing implementation?

[goldfirere]

It's true that poly- and higher-kinded datatypes don't promote, but the mechanism we're talking about works over unpromoted tycons. So, promotion isn't really part of the story here.

[jstolarek]

the mechanism we're talking about works over unpromoted tycons

Duh, I forgot about that. That's certainly a good reason not to do it during promotion. So the plan is to completely remove that implementation and just give the user access to TyConX? Are you working on th-desugar switch or can I fix that tomorrow?

[goldfirere]

Yes, that's the plan for now. I'm sorry that you put time into this idea, which was my suggestion, only for me to rescind it. I'm in the middle of the th-desugar rollover, so I request a freeze on any code changes. Perhaps I'll finish the rollover tomorrow (Wed), but perhaps not. I'll let you know when the freeze is lifted. Thanks!

On Apr 1, 2014, at 2:24 PM, Jan Stolarek notifications@github.com wrote:

the mechanism we're talking about works over unpromoted tycons

Duh, I forgot about that. That's certainly a good reason not to do it during promotion. So the plan is to completely remove that implementation and just give the user access to TyConX? Are you working on th-desugar switch or can I fix that tomorrow?

— Reply to this email directly or view it on GitHub.

[goldfirere]

I think this feature is gone, in favor of the TyCon stuff. Closing...