Skip to content

GitLab

Open
Created by Krzysztof Gogolewski@monoidalDeveloper

Linear types: investigate the multiplicity argument of FUN

Currently, the kind of FUN is

forall (m :: Multiplicity) -> forall {r1 r2 :: RuntimeRep}. Multiplicity -> 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.

  1. Multiplicity -> forall {r1 r2 :: RuntimeRep}. TYPE r1 -> TYPE r2 -> Type

    I could not get this to work with Typeable, which discards toplevel foralls to get rid of kind polymorphism.

  2. 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-in type (->) @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.