I have a typeclass that looks like this:
module Observation where import Prelude import Prelude qualified as P ((+)) class Observation f a where konst : a -> f a (+) : f a -> f a -> f a (===): f a -> f a -> f Bool
This generates an expression tree, which I would like to be able to serialize to the ledger. I can use it to write expression such as:
(kons 1 + kons 2) === konst 3
To achieve this, I’ve taken the approach similar to that described in Functions - Can we pass them as arguments in a choice? , of encoding it as a data type
instance Observation Obs a where konst = Const (+) = Add (===) = Equals -- FAILS TO COMPILE data Obs a = Const a | Add with lhs: Obs a, rhs: Obs a | Equals with lhs: Obs a, rhs: Obs a
Now this doesn’t work - error on the implementation of
(===) = Equals. The reason is that in the typeclass, this requires a return type of
Obs Bool, but the ADT constructor
Equals infers an
This is practically the motivating problem described for
GADTs in the Haskell wiki. This language feature doesn’t quite work in DAML unfortunately.
@cocreature Also suggested I look at using a different encoding using the Yoneda lemma. An example is given in this blog post, about half way down the page. But you’ll notice the transformation embeds a function into the ADT, which is not serializable, so that doesn’t help.
I also considered splitting up the algebra in two, with boolean algebra looking something like this:
data Boolean = Equals : forall a . (Obs a, Obs a) ...
You’ll notice this data type doesn’t have a type parameter
a so it’s not inferred. But this also requires a language feature that isn’t supported.
Finally, I should mention that there are a couple of not-so-great solutions, such as ‘tagging’ the type
a, by using e.g.
Either a Bool instead. This has the major disadvantage that writing expressions will no longer warn of type errors at compile-time. For example, the expression
Left 1 === Right false
would compile fine (although it would throw an error at runtime).
I’m fresh out of ideas. Could anybody suggest an alternative approach?