haskelltypesidrislinear-types

Why does Haskell 9.0 not have Zero in its linear types, but Idris 2 does?

From the Idris 2 publication about linear types "Idris 2: Quantitative Type Theory in Practice":

For Idris 2, we make a concrete choice of semiring, where a multiplicity can be one of:

  • 0: the variable is not used at run time
  • 1: the variable is used exactly once at run time
  • ω: no restrictions on the variable’s usage at run time

But for Haskell:

In the fashion of levity polymorphism, the proposal introduces a data type Multiplicity which is treated specially by the type checker, to represent the multiplicities:

data Multiplicity
  = One    -- represents 1
  | Many   -- represents ω

Why didn't they add a Zero?

Solution

  • In Idris, the value of a function argument can appear in the return type. You might write a function with type

    vecLen : (n : Nat) -> Vect n a -> (m : Nat ** n = m)

    This says "vecLen is a function that takes a Nat (call it n) and a Vect of length n and element type a and returns a Nat (call it m) such that n = m". The intent is to walk the linked list Vect and come up with its length as a runtime Nat value. But the issue is that vecLen requires you to already have the length of the vector as a runtime value, because that's the very n argument we're talking about! I.e. it's possible to implement just

    vecLen n _ = (n ** Refl) -- does no real work

    You can't not take n as an argument, because the Vect type needs its length as an argument to make sense. This is a somewhat serious problem, because having both n and a Vect n a duplicates information—without intervention the "classic" definition of Vect n a itself is in fact space-quadratic in n! So we need a way to take an argument that we know "in principle exists" but may not "actually exist" at runtime. That's what the zero multiplicity is for.

    vecLen : (0 n : Nat) -> Vect n a -> (m : Nat ** n = m)
-- old definition invalid, you MUST iterate over the Vect to collect information on n (which is what we want!)
vecLen _ [] = (0 ** Refl)
vecLen _ (_ :: xs) with (vecLen _ xs)
    vecLen _ (_ :: xs) | (n ** Refl) = (S n ** Refl)

    This is the use of the zero multiplicity in Idris: it lets you talk about values that may not exist yet/anymore/ever inside of types so you can reason about them etc. (I believe in one talk Edwin Brady did, he used or at least noted you could use zero multiplicities to reason about the previous state of a mutable resource.)

    But Haskell does not quite have this kind of dependent typing... so there just isn't a use case for zero multiplicities. From another point of view, the zero multiplicity form of f :: a -> b is just f :: forall (x :: a). b, because Haskell is wholesale type-erased in a way that Idris and other dependently typed languages cannot easily be. (In this sense, IMO, I think Haskell has the whole dependent type erasure problem that other languages have such trouble with neatly solved—at the cost of having to use an awkward encoding for everything else about dependent types!)

    In the latter sense, the "dependent" Haskell (i.e. souped-up with singletons) way to take a dependent, unrestricted argument is this:

    --        vvvvvv +  vvvvvvvv duplicate information!
vecLen :: SNat n -> Vect n a -> SNat n
vecLen n _ = n -- allowed, ergh!

    and the "zero multiplicity" version is just

    vecLen :: Vect n a -> SNat n
-- must walk Vect, cannot match on erased types like n
vecLen Nil = SZ
vecLen (_ `Cons` xs) = SS (goodLen xs)