Reading typeclass constraints

A “normal” Daml function’s type has the form

X -> Y -> Z

where X and Y are argument types, and Z is the result type, all separated by ->

But there are many definitions in Daml that have a different symbol, =>. Like so:

C => Z

where Z might have some -> of its own. It looks sort of like a function type, but most of the time the call of the function contains no reference whatsoever to C.

So what is this thing? We call the part before the => a constraint, or typeclass constraint in common parlance.

One of the interesting properties of this whole constraint system is that aside from its appearance in type errors, you don’t really have to understand it until you’re ready to understand it. So if you’re a new Daml user, maybe don’t worry too much about anything in this article. If you want to know, though, here it is.

Type variables without constraint

A typical generic function—one that can work with many types, not just one set of argument and result types—might be map, whose signature is

map : (a -> b) -> [a] -> [b]

The way to read this signature is “I can substitute any type I want for a and b, as long as I do it consistently.” So all of these are valid uses of map:

(Int -> Int) -> [Int] -> [Int]
(Int -> Text) -> [Int] -> [Text]
(ContractId IouTransfer -> ContractId Iou) -> [ContractId IouTransfer] -> [ContractId Iou]

Moreover, the function will behave consistently, no matter what types you substitute; it will not do something different just because you’ve set b = Text rather than b = Int.

By contrast, this is an invalid expansion, because it does not set b consistently across the type signature:

(Int -> Text) -> [Int] -> [ContractId Iou]

That said, you can pick any types you want for a and b.

However, consider what that would mean for the create function from the Daml standard library, if it was typed like this:

create : t -> Update (ContractId t)

This works fine for templates like Iou and IouTransfer. However, according to our rule for setting type variables, it also allows something like

Int -> Update (ContractId Int)
Text -> Update (ContractId Text)

However, it doesn’t make sense to create an Int or Text; they aren’t templates, so you can’t have contracts on the ledger with them. They don’t even have signatories. We wouldn’t even know where to start creating an Int contract.

We can’t take out the type variable, because create must work for many types, all template types in fact. We just don’t want it to work for all types. So we want some way to constrain the t type variable to allow template types like Iou, but disallow types in general.

Reading a single constraint

In reality, create has the signature

create : (HasCreate t) => t -> Update (ContractId t)

If you want to understand “by example”, as it were, the approach is always the same: substitute concrete types for the type variables and see if it makes sense.

What if we wrote some template Iou and tried to create it? We set t = Iou to match the argument type we pass to create, and the signature becomes

(HasCreate Iou) => Iou -> Update (ContractId Iou)

Remembering that our call never mentions what’s before the =>, this function takes an Iou payload and returns a ledger action that yields a ContractId Iou.

By contrast, consider what happens if we set t = Int:

(HasCreate Int) => Int -> Update (ContractId Int)

This is well-kinded in the language of types, as it were—it correctly defines a type—but creating an Int contract doesn’t make sense. Int wasn’t defined with template.

Typeclasses classify types

How do we make it so that you can set t = Iou, or any other template type for that matter, but reject t = Int as it is not something you can create? The answer is in the constraint.

In the first case, we have HasCreate Iou. In the second we have HasCreate Int. If we try the latter, we get

daml> create 42
  <string>:1:1: error:
  • No instance for (HasCreate Int) arising from a use of ‘create’

The first HasCreate exists, and the second one doesn’t. That’s how we figure out there’s an error, and report it.

First and foremost, typeclasses classify types. For every type t, either HasCreate t exists, or it does not; there is no in-between. Moreover, this is a fact about the compile-time type, not about “objects”, a runtime concept; we answer this question while compiling code, and it is never an ambiguous answer.

HasCreate Iou exists, and HasCreate Int does not. So the constraint is solved in the first case, and not solved in the second. That’s because, in the HasCreate typeclass, the typeclass instance HasCreate Iou exists, but there is no instance for HasCreate Int.

So how can we read create : (HasCreate t) => t -> Update (ContractId t)? “create has a function type that takes a t as an argument and returns a ledger action that yields a ContractId t, where type t ‘has a create’.”

Longer constraints

Let’s consider a longer signature. When you break these down into their parts, they’re not as scary as they look.

createAndExercise :
(HasCreate t, HasExercise t c r) => t -> c -> Update r

First, a compound constraint (a, b, c, …) is exactly the sum of its parts. To understand the constraint (HasCreate t, HasExercise t c r), you only have to understand what HasCreate t and HasExercise t c r mean separately.

Given that, let’s read the type. “Given a t and c, where t can be created, and exercising choice c on contracts of type t will return r, return a ledger action that yields r.”

Two wrinkles remain here. First, I’ve said that typeclasses classify types, and that remains true even when a typeclass has three type parameters, like HasExercise t c r. The difference is that HasCreate classifies single types: a type is either in the class, or it is not. HasExercise classifies triples of types: any list of 3 types is either in the class, or it is not.

-- so given the Iou choice
choice Iou_Transfer : ContractId IouTransfer

-- this is in the class HasExercise
t = Iou
c = Iou_Transfer
r = ContractId IouTransfer

-- and substituting these for the createAndExercise type, we get
(HasCreate Iou,
 HasExercise Iou Iou_Transfer (ContractId IouTransfer))
=> Iou -> Iou_Transfer -> Update (ContractId IouTransfer)

-- since the constraints can be resolved,
-- everything before the => then goes away

A typeclass is its types and values

The second wrinkle is, how can we interpret HasExercise t c r as “exercising choice c on contracts of type t will return r”?

A typeclass is two things put together:

  1. the types that are part of it, and
  2. the values listed under its class declaration.

So we can figure out how to read the constraint by looking at those two things.

First, let’s look at (2), the definition of HasExercise. We can find it in the Daml docs:

class HasExercise t c r where
    exercise
        : ContractId t -> c -> Update r

That’s enough to tell us we’re operating on contracts of template type t, and that the result is a ledger operation returning r.

What about c, which could be anything, looking at this signature? We can take a hint from the documentation for exercise, “Exercise a choice on the contract with the given contract ID.” Answering the question of “what is HasExercise”, (2) is just this exercise method. So understanding what this sole method does is all we need to know in that respect.

To figure out (1), the types that are part of HasExercise, we could look at some examples. In every example you’ll find, the second argument is some choice on the template of the contract identified by the contract ID.

We can test our assumptions in Daml Studio, though. Try adding to a Daml file alongside Iou:

foo = exercise @Int @Int
-- red-line error
error:
    • No instance for (HasExercise Int Int r0)
        arising from a use of ‘exercise’
    • In the expression: exercise @Int @Int

We can do this because the first two type arguments are t and c, which correspond to what we might hypothesize are the template type and choice type.

However, plug in this instead:

foo = exercise @Iou @Iou_Transfer
-- and daml studio will have no errors, and even have the line above
foo : ContractId Iou -> Iou_Transfer -> Update (ContractId IouTransfer)
-- which shows by absence of the `HasExercise` constraint
-- that it was successfully resolved

-- We can check our understanding of r, too:
foo = exercise @Iou @Iou_Transfer @(ContractId IouTransfer)
-- which shows exactly the same inferred foo type as above.

-- Put in something wrong like @Int and we get
error:
    • Couldn't match type ‘ContractId IouTransfer’ with ‘Int’
        arising from a functional dependency between:
          constraint ‘HasExercise Iou Iou_Transfer Int’
            arising from a use of ‘exercise’
          instance ‘HasExercise Iou Iou_Transfer (ContractId IouTransfer)’

These are all various ways the Daml compiler has of explaining

  1. There are no HasExercise instances where (t = Int, c = Int);
  2. there is an instance where t = Iou, c = Iou_Transfer, and r = ContractId IouTransfer;
  3. there are no instances for any other r, such as Int, where t = Iou and c = Iou_Transfer.

Since there is no deeper meaning of HasExercise to plumb beyond its types and its methods, we’ve done more than enough to safely interpret HasExercise t c r as “exercising choice c on contracts of type t will return r”.

Constraint aliases are only the sum of their constraints

Sometimes we like to bundle constraints under names in the standard library. You can do this too:

type Template t
    = (HasSignatory t, HasObserver t, HasEnsure t, HasAgreement t,
       HasCreate t, HasFetch t, HasArchive t, HasTemplateTypeRep t,
       HasToAnyTemplate t, HasFromAnyTemplate t)

Again, I discourage reading too much into the name Template here. This constraint means exactly the same as the 10 listed constraints to the right of the =, no more and no less. Any type that satisfies all 10 constraints will also satisfy Template t, and vice versa. So when such an alias occurs in a type you are trying to read, you need only read the component parts to understand what the whole constraint means.

A longer example, and exercise

With the above ideas in our toolkit, we can read a signature like queryContractKey from the Daml.Trigger library.

(Template a,         -- Given 'a', a template type,
 HasKey a k,         -- where 'a's key type is k,
 Eq k,               -- and 'k's can be compared for equality,
 ActionTriggerAny m, -- and 'm' is an action type for a trigger’s initialize, updateState, or rule,
 Functor m)          -- which can also be mapped from one result type to another:
=> k                 -- a function that takes a k
-> m (Optional (ContractId a, a))
-- and returns either a pair of an 'a' contract ID and payload or nothing,
-- resulting from an m action

I’ll leave determining how I translated these as an exercise for you. The understanding tools I’ve discussed in this article are your guide to making these same determinations.

Rules of thumb

Some key elements to keep in mind:

  1. To make an abstract type concrete, substitute concrete types for the type variables and see if your substitution makes sense.
  2. If a constraint can be satisfied by the Daml compiler, the chosen types are in the class. If it cannot, the types are not in the class.
  3. A compound constraint (a, b, c) is exactly the sum of its elements, no more, no less.
  4. A typeclass consists only of the types that are part of it, and the values listed under its definition.
  5. You can always ask Daml Studio whether a set of types is in a typeclass.

This article was tested with Daml SDK 2.0.0. It arose out of this discussion of documenting design with typeclasses; thanks to @Leonid_Rozenberg and @asarpeshkar for the inspiration.

I welcome suggestions to improve this tutorial’s clarity, but would rather restrain its scope as-is and leave the bigger questions to other documents. If you find it valuable as a Daml developer, please say so, and we may invest time into documenting more typeclass-related topics.

9 Likes

This is an excellent introduction. One suggestion-you might want to start off with a brief introduction to the unconstrained case, i.e parametric polymorphism without type-classes. This motivates the solution (type-classes), as without a constraint you don’t get ad-hoc polymorphism, so you can’t write functions whose behavior varies by type.

A big enough topic to be a whole separate document, I would say. :+1:

Thinking about this a bit more, it might be worth introducing the mechanism of substituting for type variables as a bit of front-matter.

I’ve added a new leader section, “Type variables without constraint”. What do you think?

1 Like

I quite like it, I think it does a good job at motivating type classes. I think it would be nice if it also mentioned and explained type applications (e. g. exercise @Iou @Iou_Transfer) as a mechanism for setting the variables in a type, since you use it later in A typeclass is its types and values

1 Like

One other thing that comes to mind is the distinction between implementing ad-hoc polymorphism via type-classes vs subtyping:

  1. Because type-inference finds a substitution for each type-variable whether or not it’s constrained, type-classes don’t lose information. Given a function f : SomeClass a => a -> a, the compiler will find a concrete type for a at each call site. If there is a SomeClass Bar instance and a function g : Bar -> Int then g $ f someBar is valid. In a language with subtyping the analog would be f : SomeSuperType -> SomeSuperType and g $ f someBar won’t typecheck even if Bar is a subtype of SomeSuperType–you need to insert a cast.
  2. Type-classes are open, in that you can add behavior to existing types that you don’t own.

I think (2), in particular, is worth emphasizing for programmers coming from OO languages.