Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Instantiating type constructors with different arities in functors #8730

Open
bobot opened this issue Jun 11, 2019 · 5 comments

Comments

@bobot
Copy link
Contributor

commented Jun 11, 2019

The arities of types in functor actual arguments must match the one of the formal argument of the functor. So this simplified version of the Set.Make functor of the standard library can be applied to I but not to T1 and T2.

module Make0(X: sig type t val compare: t -> t -> int): sig
  type t
  val singleton: X.t -> t
end

module I = struct
   type t = int
   let compare x y = Pervasive.compare x y
end

module T1 = struct
   type 'a t = { tag: int; data1: 'a }
   let compare x y = Pervasive.compare x.tag y.tag
end

module T2 = struct
   type ('a,'b) t = { tag: int; data1: 'a; data2: 'b; }
   let compare x y = Pervasive.compare x.tag y.tag
end

The implementation of Make0 can be copied unchanged except for the addition of type argument to X.t and t in order to get a functor which accepts T1.

module Make1(X: sig type 'a t val compare: 'a t -> 'a t -> int): sig
  type 'a t
  val singleton: 'a X.t -> 'a t
end

But T2 can not be applied to Make1 and we need to write Make2. However contrary to Make0, the interface for Make2 can be automatically generated from the interface of Make1. It is not as simple as substituting 'a by ('a,'b), it is more to propagate through all the signature the modification of arity. This process could fail if we need to change the arity of external type constructor or if a type constructor that need to change it's arity is applied not with a type variable or if a type constructor need to change to different arities.

  val to_list: 'a t -> 'a list
  val specialized: bool X.t -> bool t

This generation of Make2 from Make1 is perhaps not the right way and the correctness of the approach is questionable. But the main feature of defining functors that are applicable to different arities is useful.

PS: I though I already reported this feature wish a long time ago, but I have not been able to find it for linking it to #8727.

@bobot

This comment has been minimized.

Copy link
Contributor Author

commented Jun 11, 2019

@mrmr1993, will #8727(or the series of PR) be able to allow easily to implement the functor once for all arities?

@mrmr1993

This comment has been minimized.

Copy link
Contributor

commented Jun 11, 2019

@bobot that's not the initial intention, no.

Once the feature is complete, it should be possible (and fairly easy?) to support partially-applied type constructors fairly easily though. The main issue will be the syntax: how will we differentiate between intentionally omitted and accidentally omitted type parameters? Still, this is certainly one of my extension goals, once we have a reasonable story for the syntax.

@bobot

This comment has been minimized.

Copy link
Contributor Author

commented Jun 11, 2019

I don't want partially-applied type, I think. Type constructor are always fully applied. The goal here is just to be able to define a functor once for an abstract type 'a t and that it would be usable for type t or type ('a,'b) t.

@mrmr1993

This comment has been minimized.

Copy link
Contributor

commented Jun 11, 2019

I don't want partially-applied type, I think.

Sorry, I misspoke. I was viewing this from the angle that the type variables needed to 'live' somewhere, so that the typechecker knows about them, and I thought something akin to a partially-applied type might be a good candidate for that.

I'm not certain what the semantics should be in terms of variable splitting: ie. should 'a t - > 'a t become '('a, 'b) t -> ('a, 'b) t, ('a, 'b) t -> ('a, 'c) t, etc. Even moreso for types with higher arities. Did you have a plan for this?

@bobot

This comment has been minimized.

Copy link
Contributor Author

commented Jun 11, 2019

The signature 'a t - > 'a t would become ('a, 'b) t -> ('a, 'b) t. The 'a in the first signature can be seen as a variable for a list of type variables and so the first signature says that the list of type variable is the same in input and output. I think this view applies to higher arities directly.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
2 participants
You can’t perform that action at this time.