Linear types: investigate the multiplicity argument of FUN
Currently, the kind of FUN
is
forall (m :: Multiplicity) -> forall {r1 r2 :: RuntimeRep}. TYPE r1 -> TYPE r2 -> Type
This is a hack. The argument m
is dependent, even though it is not used as such.
The goal of this ticket is to investigate how to simplify this and make m
non-dependent. There are two candidates; I prefer the second one.
-
Multiplicity -> forall {r1 r2 :: RuntimeRep}. TYPE r1 -> TYPE r2 -> Type
I could not get this to work with
Typeable
, which discards toplevelforall
s to get rid of kind polymorphism. -
forall {r1 r2 :: RuntimeRep}. Multiplicity -> TYPE r1 -> TYPE r2 -> Type
During the implementation of linear types, I was worried that with this option
type (->) = FUN 'Many
would no longer support levity polymorphism. However, this should be doable with a built-intype (->) @r1 @r2 = FUN @r1 @r2 'Many
.
One consequence of this hack is that the implementation of Typeable
with linear types is more complicated. Previously, the TypeRep for ((->) x) y
was stored using a separate constructor TrFun
as a mere optimisation. Now, TrFun
is an irreducible primitive remembering the multiplicity. This ticket should restore the previous state, and furthermore it should be possible to remove the restriction "splitApps: Only unrestricted functions are supported"
in Typeable.
This ticket is best done after #18750.