Implicit arguments

In programming languages with sophisticated type systems we easily run into inconvenience of providing many (often type) arguments explicitly. Let's take a simple map function as an example:

map :: forall a b. (a -> b) -> List a -> List b

If we had to always explicitly provide map's arguments, write something like

ys = map @Char @Char toLower xs

we would immediately give up on types, and switch to use some dynamically typed programming language. It wouldn't be fun to state "the obvious" all the time.

Fortunately we know a way (unification) which can be used to infer many such argument. Therefore we can write

ys = map toLower xs

and the type arguments will be inferred by compiler. However we usually are able to be explicit if we want or need to be, e.g. with TypeApplications in GHC Haskell.

#Beyond Hindley-Milner

Conor McBride calls a following phenomenon "Milner's Coincidence":

The Hindley-Milner type system achieves the truly awesome coincidence of four distinct distinctions

• terms vs types
• explicitly written things vs implicitly written things
• presence at run-time vs erasure before run-time
• non-dependent abstraction vs dependent quantification

We’re used to writing terms and leaving types to be inferred. . . and then erased. We’re used to quantifying over type variables with the corresponding type abstraction and application happening silently and statically.

GHC Haskell type-system has been long far more expressive than vanilla Hindley-Milner, and the four distrinctions are already misaligned.

GHC developers are filling the cracks: For example we'll soon ¹ get a forall a -> (with an arrow, not a dot) quantifier, which is erased (irrelevant), explicit (visible) dependent quantification. Later we'll get foreach a. and foreach a -> which are retained (i.e. not-erased, relevant) implicit/explicit dependent quantification.

(Agda also has "different" quantifiers: explicit (x : A) -> ... and implicit {y : B} -> ... dependent quantifiers, and erased variants look like (@0 x : A) -> ... and {@0 y : B} -> ....)

In Haskell, if we have a term with implicit quantifier (foo :: forall a. ...), we can use TypeApplications syntax to apply the argument explicitly:

bar = foo @Int

If the quantifier is explicit, we'll (eventually) write just

bar = foo Int

or

bar = foo (type Int)

for now.

#Inferred type variables

That all is great, but consider we define a kind-polymorphic² type like

type ProxyE :: forall k. k -> Type
data ProxyE a = MkProxyE

then when used at type level, forall behaves as previously, constructors

ghci> :kind ProxyE Int
ProxyE Int :: Type

ghci> :kind ProxyE @Type Int
ProxyE @Type Int :: Type

The type of constructor MkProxyE is

ghci> :type ProxyE
ProxyE :: forall k (a :: k). ProxyE @k a

So if we want to create a term of type Proxy Int, we need to provide both k and a arguments:

ghci> :type ProxyE @Type @Int
ProxyE @Type @Int :: ProxyE @(Type) Int

we could also jump over k:

ghci> :type MkProxyE @_ @Int
MkProxyE @_ @Int :: ProxyE @(*) Int

The above skipping over arguments is not convenient, luckily GHC has a feature, created for other needs, which we can (ab)use here. There are inferred variables (though the better name would be "very hidden"), these are arguments for which TypeApplication doesn't apply:

type Proxy :: forall {k}. k -> Type
data Proxy a = MkProxy

This is the way Proxy is defined in base (but I renamed the constructor to avoid name ambiguity)

And while GHCi prints

ghci> :type MkProxy @Int
MkProxy @Int :: Proxy @{Type} Int

the @{A} syntax is not valid Haskell, so we cannot explicitly apply inferred variables. Neither we can in types:

ghci> :kind! Proxy @{Type}

<interactive>:1:10: error: parse error on input ‘Type’

I think this is plainly wrong, we should be able to apply these "inferred" arguments too.

The counterargument is that, inferred variables weren't meant to be "more implicit" variables. As GHC manual explains, inferred variables are a solution to TypeApplications with inferred types. We need to know the order of variables to be able to apply them; but especially in presence of type-class constraints the order is arbitrary.

I'm not convinced, I think that ability to be fully explicit is way more important than a chance to write brittle code.

One solution, which I think would work, is simply to not generalise. This is controversial proposal, but as GHC Haskell is moving towards having fancier type system, something needs to be sacrificed. (MonoLocalBinds is for local bindings, but I'd argue that should be for all bindings, not only local).

The challenge has been that library writes may not been aware of TypeApplications, but today they have no choice. Changing from foo :: forall a b. ... to foo :: forall b a. ... may break some code (even though PVP doesn't explicitly write that down, that should be common sense).

So in the GHC manual example

f :: (Eq b, Eq a) => a -> b -> Bool
f x y = (x == x) && (y == y)

g x y = (x == x) && (y == y)

the g would fail to type-check because there are unsolved type-variables. One way to think about this is that GHC would refuse to pick an order of variables. GHC could still generalise if there are no dictionary arguments, but on the other hand I don't think it would help much. It might help more if GHC wouldn't specialise as much, then

h = f

would type-check.

This might sound like we would need to write much many type signatures. I don't think that is true: it's already a best practice to write type signatures for type level bindings, and for local bindings we would mostly need to give signatures to function bindings.

This proposal subsumes monomorphism restriction, recall that without type defaulting:

-- turn off defaulting
default ()
fooLen = genericLength "foo"

will fail to compile with

Ambiguous type variable ‘i0’ arising from a use of ‘genericLength’
prevents the constraint ‘(Num i0)’ from being solved.

error. With NoMonomophismRestriction we have

ghci> :t fooLen
fooLen :: Num i => i

Another, a lot simpler option, is to simply remember whether the symbols' type was inferred, and issue a warning if TypeApplications is used with such symbol in application head. So if user writes

... (g @Int @Char ...)

GHC would warn that g has inferred type, and the TypeApplications with g are brittle. The solution is to give g a type signature. This warning could be issued early in a pipeline (maybe already in renamer), so it would explain further (possibly cryptic) type errors.

Let me summarise the above: If we could apply inferred variables, i.e. use curly brace application syntax, we would have complete explicit forall a ->, implicit forall a. and more implicit forall {a}. dependent quantifiers. Currently the forall {a}. quantifier is incomplete: we can abstract, but we cannot apply. We'll also need some alternative solution to TypeApplicaitons and inferred types. We should be able to bind these variables explicitly in lambda abstractions as well: \ a ->, \ @a -> and \ @{a} -> respectively (see TypeAbstractions).

#Alternatives

The three level explicit/implicit/impliciter arguments may feel complicated. Doesn't other languages have similar problems, how they solve them?

As far as I'm aware Agda and Coq resolve this problem by supporting applying implicit arguments by name:

-- using indices instead of parameters,
-- to make constructor behave as in Haskell
data Proxy : {k : Set} (a : k) -> Set1 where
  MkProxy : {k : Set} {a : k} -> Proxy a

t = MkProxy {a = true}

Just adding named arguments to Haskell would be a bad move. It would add another way where a subtle and well-meaning change in the library could break downstream. For example unifying the naming scheme of type-variables in the libraries, so they are always Map k v and not Map k a sometimes, as it is in containers which uses both variable namings.

We could require library authors to explicitly declare that bindings in a module can be applied by name (i.e. that they have thought about the names, and recognise that changing them will be breaking change). You would still be able to always explicitly apply implicit arguments, but sometimes you won't be able to use more convenient named syntax.

It is fair to require library authors to make adjustments so that (numerous) library users would be able to use a new language feature with that library. In a healthy ecosystem that shouldn't be a problem. Specifically it is extra fair, if the alternative is to make feature less great, as then people might not use it at all.

#Infinite level of implicitness

Another idea is to embrace implicit, more implicit and even more implicit arguments. Agda has two levels: explicit and implicit, GHC Haskell has two and a half, why stop there?

If we could start fresh, we could pick Agda's function application syntax and have

funE arg    -- explicit application
funI {arg}  -- explicit application of implicit argument

but additionally we could add

funJ {{arg}}    -- explicit application of implicit² argument
funK {{{arg}}}  -- explicit application of implicit³ argument
...             -- and so on

With unlimited levels of implicitness we could define Proxy as

type Proxy :: forall {k} -> k -> Type
data Proxy a where
    MkProxy :: forall {{k}} -> {a :: k} -> Proxy a

and use it as MkProxy, MkProxy {Int} or MkProxy {{Type}} {Int} :: Proxy Int. Unlimited possibilities.

For what it is worth, the implementation should be even simpler than of named arguments.

But I'd be quite happy already if GHC Haskell had a way to explicitly apply any function arguments, be it three levels (ordinary, @arg and @{arg}) of explicitness, many or just two; and figured another way to tackle TypeApplications with inferred types.

• 2024-04-21 – A note about coercions
• 2024-04-18 – What makes a good compiler warning?
• 2024-04-12 – Core Inspection
• 2024-04-01 – Implicit arguments
• 2024-03-17 – ST with an early exit

twitter github email linkedin stackoverflow