Documentation

The type of errors that readKnown and makeKnown can return.

A version of GEq that fixes a in place, which allows us to create an inlinable recursive implementation of geqL.

The way it works is that whenever there's recursion, we look up the recursive case in the current context (i.e. the dictionary) instead of actually calling geqL recursively (even though it's gonna look like we do exactly that, because there's no way to distinguish between a recursive call and a dictionary lookup as the two share the same name, although to help GHC choose a lookup we sprinkle the perhaps unreliable LoopBreaker in the DefaultUni instance of this class).

Alligning things this way allows us to inline arbitrarily deep recursion for as long as types keep being monomorphic.

For example, the MapData builtin accepts a [(Data, Data)] and with geqL matching on all of DefaultUniProtoList, DefaultUniProtoPair and DefaultUniData gets inlined in the denotation of the builtin. For the Constr builtin that resulted in a 4.3% speedup at the time this comment was written.

In f = ... f ... where f is a class method, how do you know if f is going to be a recursive call or a type class method call? If both type check, then you don't really know how GHC is going to play it. So we add this data type to make sure that the RHS f will have to become a type class method call.

Can GHC turn that method call into a recursive one once type classes are resolved? Dunno, but at least we've introduced an obstacle preventing GHC from immediately creating a non-inlinable recursive definition.

A constraint for "a is a ReadKnownIn and MakeKnownIn by means of being included in uni".

A constraint for "a is a ReadKnownIn and MakeKnownIn by means of being included in UniOf term".

The monad that makeKnown runs in. Equivalent to ExceptT BuiltinError (Writer (DList Text)), except optimized in two ways:

1. everything is strict
2. has the BuiltinSuccess constructor that is used for returning a value with no logs attached, which is the most common case for us, so it helps a lot not to construct and deconstruct a redundant tuple

Moving from ExceptT BuiltinError (Writer (DList Text)) to this data type gave us a speedup of 8% of total evaluation time.

Logs are represented as a DList, because we don't particularly care about the efficiency of logging, since there's no logging on the chain and builtins don't emit much anyway. Otherwise we'd have to use text-builder or text-builder-linear or something of this sort.

The monad that readKnown runs in.

A non-empty spine. Isomorphic to NonEmpty, except is strict and is defined as a single recursive data type.

The head-spine form of an iterated application. Provides O(1) access to the head of the application. NonEmpty a ~ HeadSpine a a, except is strict and the no-spine case is made a separate constructor for performance reasons (it only takes a single pattern match to access the head when there's no spine this way, while otherwise we'd also need to match on the spine to ensure that it's empty -- and the no-spine case is by far the most common one, hence we want to optimize it).

Used in built-in functions returning function applications such as CaseList.

Construct HeadSpine from head and list.

HeadSpine but the type of head and spine is same

Convert a constant embedded into a PLC term to the corresponding Haskell value.

Same as makeKnown, but allows for neither emitting nor storing the cause of a failure.

Same as readKnown, but the cause of a potential failure is the provided term itself.