The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org>]

Hi Matthieu,

Thank you for your answer. Even if this leaves us without a solution to our problem, at least we now understand it :)

--
JH

Le 12/09/2017 à 20:30, Matthieu Sozeau a écrit :

Hi,

  template polymorphic inductives can't be instantiated by universes, one could only "refresh" their type but that would only be useful for the conclusion, and even then I don't know what we could do in the kernel, the fresh universes have no place to be recorded in the representation. The domain types would still have to be convertible, e.g. list's universe i would have to be equal to the domain of Fmap's G operator in the Fmap list application. Otherwise said, template polymorphism does not go as far as making the domain of the G type constructor a "parameter" of Fmap.

Also, singleton classes like Fmap do not have template polymorphism, you'd need Class Fmap G := { fmap : ... } to declare an inductive instead of a definition, but that doesn't change the problem.

```

 Module BuiltinLists.

   Universe i.

   Class Fmap (G : Type@{i} -> Type) := fmap : forall {A B : Type@{i}} (f : A -> B) , G A

-> G B.

   Set Printing Universes.

   Instance list_Fmap : Fmap list := map.

   (* Forces lists' Datatypes.44 = i *)

   Fail Definition fails := map _ (cons list_Fmap nil).

   (* (list_Fmap : Fmap list : Type@{i+1,..) > i = Datatypes.44 *)

End BuiltinLists.

```

> What does "because there's no way to know what the fresh levels are in that case, when retyping"? Can't you just use fresh level and unify them with whatever they need to be unified with, depending on the context? Why is this a problem for template polymorphism and not for full polymorphism? Also, more fundamentally, why doesn't that break subject reduction, given that eta-reduction is part of Coq's conversion rules?

As mentioned by Guillaume, eta is only about conversion.

The difference between template and full is exactly that list (and Fmap, and map) get universe instances attached to them in the internal representation, while template polymorphic inductives need their parameters types to typecheck (i.e. we need to see list A to infer its type using template polymorphism, which will depend on A's inferred type, partial applications don't have enough information to do that). So that leaves only eta-expansion to get out of your conundrum. Your example is even worsened by the partial application of map in list_Fmap, the following works:

```

Module BuiltinListsEtaMap.

  Class Fmap (G : Type -> Type) := fmap : forall {A B} (f : A

-> B) , G A -> G B.

   Instance list_Fmap : Fmap list :=

     fun A B => @map A B.

   Definition succeeds := map id (cons list_Fmap nil). 

(* This is because map's universes are not fixed by the list_Fmap implementation in this case. However fmap id fails for the reason above *)

  Fail Definition fails := fmap id (cons list_Fmap nil). 

End BuiltinListsEtaMap.

```

You could work around it a little bit using a polymorphic class and instance,

but won't be able to "tie the knot" by applying fmap on lists containing Fmap list objects which might be what you want.

```

Module BuiltinListsEtaMap.

   Universe i.

   Polymorphic Class Fmap@{i} (G : Type@{i} -> Type@{i}) := fmap : forall {A B : Type@{i}} (f : A

-> B) , G A -> G B.

  (** This ones fully polymorphic, i is only bounded by global floating universes which are meant to go as high as necessary *)

  Polymorphic Instance list_Fmap@{i} : Fmap@{i} (fun A : Type@{i} => list A) := 

     fun A B => @map A B.

  (** This instance is for the fixed Datatypes.44 universe *)

  Instance list_Fmap' : Fmap list := list_Fmap.

  (** One can use Fmap' like this *)

  Check (fmap S (cons 0 nil)).

  (** One can use Fmap' like this *)

  Check (fmap (@tl nat) nil).

  (** But not like this, as list_Fmap' sort included the global list universe *)

  Fail Definition fail' := fmap (@id _) (cons list_Fmap' nil).

  Definition succeeds := fmap id (cons list_Fmap nil).

End BuiltinListsEtaMap.

```

Hope this helps,

-- Matthieu

On Mon, Sep 11, 2017 at 11:37 AM Jan-Oliver Kaiser <janno AT mpi-sws.org> wrote:

Here's some further illustration of the problem Jacques-Henri mentioned.
I included different variations because I had initially thought that
maybe it could be worked around by making the FMap class or instance
polymorphic. But it turns out that that doesn't help at all.

Now, the example I use doesn't make any sense on it's own but I am not
convinced that one couldn't come up with more sensible ways of
triggering universe inconsistencies in this setup.

Best,
Janno


 From Coq Require Import List.

Module BuiltinLists.
   Class Fmap (G : Type -> Type) := fmap : forall A B (f : A -> B) , G A
-> G B.

   Instance list_Fmap : Fmap list := map.


   Fail Definition fails := map _ (cons list_Fmap nil). (* sad face *)
End BuiltinLists.

Module BuiltinListsPolyClass.
   Polymorphic Class Fmap (G : Type -> Type) := fmap : forall A B (f : A
-> B) , G A -> G B.

   Instance list_Fmap : Fmap list := map.

   Fail Definition fails := map _ (cons list_Fmap nil). (* sad face *)
End BuiltinListsPolyClass.


Module BuiltinListsPolyInstance.
   Polymorphic Class Fmap (G : Type -> Type) := fmap : forall A B (f : A
-> B) , G A -> G B.

   Polymorphic Instance list_Fmap : Fmap list := map.

   Fail Definition fails := map _ (cons list_Fmap nil). (* sad face *)
End BuiltinListsPolyInstance.


Module PolyLists.
   Polymorphic Inductive list {A : Type} := | nil : list | cons : A ->
list -> list.
   Arguments list A : clear implicits.
   Polymorphic Definition map {A B : Type} (f : A -> B) := fix go l :=
match l with | nil => nil | cons a l => cons (f a) (go l) end.
   Arguments map [A B].
   Polymorphic Class Fmap (G : Type -> Type) := fmap : forall A B (f : A
-> B) , G A -> G B.

   Polymorphic Instance list_Fmap : Fmap list := map.

   Definition works := map id (cons list_Fmap nil). (* works but now we
can't use `list` from the prelude *)
End PolyLists.


On 09/06/2017 05:12 PM, Jacques-Henri Jourdan wrote:
>
> Le 06/09/2017 à 13:58, Jacques-Henri Jourdan a écrit :
>> Reason 1)
>>
>> Partially applying a template polymorphic type does not trigger
>> instantiation with fresh universe variables, and we do not understand
>> why. This issue has already been raised on this mailing list on Sat,
>> 22 Oct 2016 by Gregory Malecha in a post entitled "list :: nil?", but
>> I do not quite understand the answer. At that time, Matthieu answered :
>>
>>      >   Indeed, in the template case partial applications do not give
>> you a fresh instance (because there's no way to know what the fresh
>> levels are in that case, when retyping) , but an eta-expanded version
>> will work I think, e.g fun X => list X, as then we can look at the
>> type of X to determine the type of list X.
>>
>> What does "because there's no way to know what the fresh levels are in
>> that case, when retyping"?
>> Can't you just use fresh level and unify them with whatever they need
>> to be unified with, depending on the context?
>> Why is this a problem for template polymorphism and not for full
>> polymorphism?
>> Also, more fundamentally, why doesn't that break subject reduction,
>> given that eta-reduction is part of Coq's conversion rules?
>
> Maybe I should explain why this is a problem for us: It is not possible,
> in our case, to eta-expand the list type where it appears, because it
> appears as a parameter of a typeclass that needs to unify with
> non-eta-expanded instances of list.
>
> That is, we have a typeclass `FMap : (Type -> Type) -> Type`, and we
> want to define an instance of type `FMap list`. An instance of type
> `FMap (fun X => list X) would not work, because it would not be selected
> when searching for instances of type `FMap list`.
>

Attachment: signature.asc
Description: OpenPGP digital signature