Erased Constraint branch of compiler

[jy14898]

I decided to take a stab at implementing what I suggested in this post: Untagged union types

I don’t really expect this to make it into the official compiler, it was mostly a challenge for myself to write more haskell and develop a better understanding of the purescript compiler internals.

The basic idea is that we introduce a new type of constraint (ErasedConstraint), where the constraint must be solved for the RHS of the constraint to be used, but no dictionary is passed. The compiler guarantees to:

1. Not defer the computation in the RHS of the constraint (it never produces an abstraction which would normally introduce the instance dictionary, it’s more like a newtype)
2. Erase all ErasedConstraints before code gen, rather than applying the dictionary like a normal constraint would

The main motivation for this is for foreign imports which accept multiple types, but don’t depend on being passed instance dictionaries as they do runtime type checking (discussed in the motivating post)

I implemented this by annotating constraints with a Multiplicity, which can either be Unlimited (which is the default behavior today) and Never (meaning the dictionary is never used).

At the moment, all instances declaration produce dictionaries which are Unlimited, and Unlimited instances imply Never instances during entailment (but not the other way around). To achieve this, I modified the type NamedDict to not require a value at runtime, and therefore InstanceContext too.

Note that this doesn’t yet change built in classes like Partial, but it should be very simply to add support for them

purescript/purescript

Example code and the output:

module Main where

import Data.Unit
import Data.Show

class (Show a) <= MyShow a

ex :: forall a. Show a ? a -> Unit
ex a = unit

ex1 :: forall a. Show a => a -> Unit
ex1 a = ex a

ex2 :: forall a. MyShow a ? a -> Unit
ex2 a = ex a

test1 = ex 10
test2 = ex unit
test3 = ex1 10
test4 = ex1 unit

-- This specific example currently infers 2 constraints, when it would ideally 
-- only be 1. However, this can also happen with superclass constraints anyway
-- Could be solved by doing entailment in 2 stages, with unlimited first,
-- and then never.
-- Note that you can turn it into 1 with a hint
-- test5 :: forall a. Show a => a -> Unit
test5 a = unit
    where
          bar = show a
          foo = ex a

// Generated by purs version 0.14.0
"use strict";
var Data_Show = require("../Data.Show/index.js");
var Data_Unit = require("../Data.Unit/index.js");
var MyShow = function (Show0) {
    this.Show0 = Show0;
};
var ex = function (a) {
    return Data_Unit.unit;
};
var ex1 = function (dictShow) {
    return function (a) {
        return ex(a);
    };
};
var ex2 = function (a) {
    return ex(a);
};
var test1 = ex(10);
var test2 = ex(Data_Unit.unit);
var test3 = ex1(Data_Show.showInt)(10);
var test4 = ex1(Data_Unit.showUnit)(Data_Unit.unit);
var test5 = function (dictShow) {
    return function (a) {
        var foo = ex(a);
        var bar = Data_Show.show(dictShow)(a);
        return Data_Unit.unit;
    };
};
module.exports = {
    MyShow: MyShow,
    ex: ex,
    ex1: ex1,
    ex2: ex2,
    test1: test1,
    test2: test2,
    test3: test3,
    test4: test4,
    test5: test5
};

[timjs]

Nice work @jy14898. I like the idea of tracking which dictionaries could be erased by using multiplicities.

I’d like to suggest an improvements to make this a less intrusive language change and (hopefully!) make it more generally applicable.

Would it be possible to assign a multiplicity to a class during declaration? Classes without any members would have multiplicity Zero/Never as would built in classes like Partial and Coercible. All other classes would have multiplicity Unlimited/Always.

This would mean that in function declarations, we’d still use => instead of ?, no need to change this.

Multiplicities could be tracked by parametrising the Constraint kind with a data Multiplicity = Zero | Unlimited or data Usage = Never | Always. Alternatively, this could be implemented as an annotation on classes, if PureScript will get an annotation mechanism.

It think that for now, empty classes and built in classes with multiplicity Zero/Never would be enough. I don’t know if there are other uses cases than that from the top of my head. Type level functions using fundeps, for example, don’t have function members too.

[jy14898]

I’d probably throw in multiplicity annotations with the kind annotations, eg:

class Show :: forall (m :: Multiplicity). Type -> Constraint m
class Show a where ...

class Partial :: Constraint Never

Whether or not we’d allow quantifying the m in that way I’m not sure, because then it would be ambiguous as to which multiplicity the user wants when using the constraint. As it currently stands though, Constraint Unlimited would be the same as doing that anyway I think (and thus Unlimited would be the default when used)

Part of the reason for adding a new syntax (?) was that I could limit where these multiplicities appear, as currently the branch I made doesn’t support erased constraints in instance heads or superclass implications declarations (although superclass implications are respected when searching for instances). I don’t think there’s any fundamental reason why it couldn’t be supported without the new syntax and everywhere, but I personally also like the separation of => and ? as the former makes no guarantees about runtime representation (I believe), whereas the latter does

[natefaubion]

I’m not sure you would want to parameterize the Constraint kind, but instead you’d want to parameterize the => arrow, in a similar vein as linear types in Haskell. That’s to say, any constraint that has runtime proof can be erased if you don’t care (as a consumer), and any constraint that has no runtime proof can be provided the null dictionary. Parameterizing the arrow lets you state explicitly as a constraint consumer what you care about.

[timjs]

That’s true, it’s theoretically truer. However, is it as ergonomic and will it extend possible use cases? I mean, if a class doesn’t have methods, it’s clear it can be erased. On the other hand, if a function has a constraint on its type, but it doesn’t use any methods provided by the class, it can also be erased. But why put the constraint there in the first place, if you’re not using any methods and the method set is not empty? Is there a use case for that?

[natefaubion]

The compiler already erases empty dictionaries, it just doesn’t remove the function abstraction. This is because it changes evaluation semantics (things would not be deferred which otherwise would be due to an abstraction) and because we want to support constraint polymorphism at some point, which requires a uniform representation for =>. If you parameterize the =>, then it’s not an issue, but otherwise the representation of => depends on the kind of the constraint, which would be problematic.

[timjs]

Hmm, I see. But as PureScript is strict, should developers rely on the fact that dictionaries are passed as function arguments at runtime? It seems an implementation detail to me, which we’re exposing now. And because it is exposed, we can only erase empty dictionaries, but not the function abstraction. So it hinders optimisations.

Then, can you give me an example of constraint polymorphism? I’m familiar with constraint kinds and quantified constraints, but polymorphism over constraints seems strange to me at first thought: “This function should work for any constraint c I’ll give you, but you can’t use any methods of that class, because it’s polymorphic?” Probably shouldn’t think about it in this way

[natefaubion]

@timjs

Then, can you give me an example of constraint polymorphism? I’m familiar with constraint kinds and quantified constraints, but polymorphism over constraints seems strange to me at first thought: “This function should work for any constraint c I’ll give you, but you can’t use any methods of that class, because it’s polymorphic?” Probably shouldn’t think about it in this way

Constraint polymorphism means that you can abstract over some constraint. It’s a first-class member of the type system. See https://hackage.haskell.org/package/constraints-0.13/docs/Data-Constraint.html

With 0.14 we have a Constraint kind, but constraints are still first-order. You can only use them in certain places syntactically (for example, not as the RHS of a type synonym) and they must be fully saturated.

[natefaubion]

@timjs

Hmm, I see. But as PureScript is strict, should developers rely on the fact that dictionaries are passed as function arguments at runtime? It seems an implementation detail to me, which we’re exposing now. And because it is exposed, we can only erase empty dictionaries, but not the function abstraction. So it hinders optimisations.

Just being strict hinders a lot of optimizations if you want to preserve termination (eg maybe (unsafeCrashWith "wat") k). => has a very simple denotation at the value level as an implicit function quantifier. You can still do optimizations (just general inlining would erase a lot of these abstractions), and I’d say that elaboration to function abstractions can be helpful for optimizations (like using purescript-call-by-name for the aforementioned maybe).