Encoding inequalities in an ADT

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 Obs:

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 Obs a.

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?

Do you need the genericity afforded by type classes and type parameters here? If not, here is what I would consider a simpler approach, which seems just as type-safe to me (disclaimer: I like dynamic languages, I may not be qualified to judge type safety).

module Main where

import Daml.Script

-- Note: using dummy names for fields as they (the names) won't be used.
data BoolOp
  = ArithEqual { _a1: Op, _a2: Op }
  | BoolEqual { _b1: BoolOp, _b2: BoolOp }
  | GreaterThan { _c1: Op, _c2: Op }

data Op
  = Add { _d1: Op, _d2: Op }
  | Constant Int

eval: BoolOp -> Bool
eval = \case
  ArithEqual left right -> evalOp left == evalOp right
  BoolEqual left right -> eval left == eval right
  GreaterThan left right -> evalOp left > evalOp right

evalOp: Op -> Int
evalOp = \case
  Add left right -> evalOp left + evalOp right
  Constant i -> i

setup : Script ()
setup = script do
  assert(eval (BoolEqual (ArithEqual (Constant 1) (Constant 1))
                         (GreaterThan (Add (Constant 1) (Constant 10))
                                      (Constant 2))))

You can’t express a syntax tree consisting of an unbounded set of types in a single DAML type. Every type you can get your hands on using pattern matching has to be contained in your type somehow. Ie since you want to be able to get your hands on a value of type a by traversing the syntax tree of the result of ===, the type of that result has to contain a somehow.

If you don’t need to be serializable, you can just compose functions, swallowing types as you go, but I suspect you want something serializable. In that case, @Gary_Verhaegen’s suggestion is the way to go. Suppose I wanted such a tree where I can store Int, Text or Bool :

module Main where

import Daml.Script

class Observation f a where
  konst : a -> f a
  add : f a -> f a -> f a
  (===): f a -> f a -> f Bool

data Obs a b c d
  = Const d
  | Add (Obs a b c d, Obs a b c d)
  | EqualsA (Obs a b c a, Obs a b c a)
  | EqualsB (Obs a b c b, Obs a b c b)
  | EqualsC (Obs a b c c, Obs a b c c)

instance Observation (Obs a b c) a where
  konst = Const
  add = curry Add
  (===) = curry EqualsA

instance Observation (Obs a b c) b where
  konst = Const
  add = curry Add
  (===) = curry EqualsB

instance Observation (Obs a b c) c where
  konst = Const
  add = curry Add
  (===) = curry EqualsC

reduceObs : (Semigroup a, Semigroup b, Semigroup c, Semigroup d, Eq a, Eq b, Eq c) => Obs a b c d -> Either d Bool
reduceObs o = case o of
  Const x -> Left x
  Add (x, y) -> case (reduceObs x, reduceObs y) of
    (Left x', Left y') -> Left (x' <> y')
    (Right x', Right y') -> Right (x' <> y')
    _ -> error "IMPOSSIBLE"
  EqualsA (x, y) -> case (reduceObs x, reduceObs y) of
    (Left x', Left y') -> Right (x' == y')
    (Right x', Right y') -> Right (x' == y')
    _ -> error "IMPOSSIBLE"
  EqualsB (x, y) -> case (reduceObs x, reduceObs y) of
    (Left x', Left y') -> Right (x' == y')
    (Right x', Right y') -> Right (x' == y')
    _ -> error "IMPOSSIBLE"
  EqualsC (x, y) -> case (reduceObs x, reduceObs y) of
    (Left x', Left y') -> Right (x' == y')
    (Right x', Right y') -> Right (x' == y')
    _ -> error "IMPOSSIBLE"

instance Semigroup Int where
  (<>) = (+)

instance Semigroup Bool where
  x <> y = (x && not y) || (not x && y)

test = script do
  let
    obs : Obs Int Text Bool Bool = ((konst 1 `add` konst 2) === konst 3) `add` ((konst "1" `add` konst "2") === konst "12")
  return (reduceObs obs)

Hi @bernhard,

I must say I am still confused by the type class there. It seems a bit weird to constrain all your types to support the exact same set of operations, and it’s not clear to me what you gain in exchange for that constrain (and the additional complexity introduced by the type parameters).

If you know the types you support in advance, is it not simpler to just encode them directly? I’d go for a variant for each such type, where the variant groups all the operations that return that type.

module Main where

import Daml.Script
import qualified DA.Text

-- Note: using dummy names for fields as they (the names) won't be used.
data BoolOp
  = NumEqual { _bo1: NumOp, _bo2: NumOp }
  | BoolEqual { _bo3: BoolOp, bo4: BoolOp }
  | StringEqual { _bo5: StringOp, bo6: StringOp }
  | GreaterThan { _bo7: NumOp, _bo8: NumOp }
  | StringToBool StringOp

data NumOp
  = Add { _no1: NumOp, _no2: NumOp }
  | Num Int
  | StringToNum StringOp

data StringOp
  = Concat { _so1: StringOp, _so2: StringOp }
  | String Text
  | NumToString NumOp
  | BoolToString BoolOp

evalBool: BoolOp -> Either Text Bool
evalBool = \case
  NumEqual n1 n2 -> do
    n1' <- evalNum n1
    n2' <- evalNum n2
    return $ n1' == n2'
  BoolEqual b1 b2 -> do
    b1' <- evalBool b1
    b2' <- evalBool b2
    return $ b1' == b2'
  StringEqual s1 s2 -> do
    s1' <- evalString s1
    s2' <- evalString s2
    return $ s1' == s2'
  GreaterThan n1 n2 -> do
    n1' <- evalNum n1
    n2' <- evalNum n2
    return $ n1' > n2'
  StringToBool s -> do
    s' <- evalString s
    case s' of
      "true" -> return True
      "false" -> return False
      _ -> Left $ "Invalid conversion from String to Boolean: " <> s'

evalString: StringOp -> Either Text Text
evalString = \case
  Concat s1 s2 -> do
    s1' <- evalString s1
    s2' <- evalString s2
    return $ s1' <> s2'
  String s -> return s
  NumToString n -> do
    n' <- evalNum n
    return $ show n'
  BoolToString b -> do
    b' <- evalBool b
    return $ show b'

evalNum: NumOp -> Either Text Int
evalNum = \case
  Add n1 n2 -> do
    n1' <- evalNum n1
    n2' <- evalNum n2
    return $ n1' + n2'
  Num n -> return n
  StringToNum s -> do
    s' <- evalString s
    case DA.Text.parseInt s' of
      None -> Left $ "cannot parse as Num: " <> s'
      Some i -> return i

setup : Script ()
setup = script do
  assert(Right True == evalBool (BoolEqual (NumEqual (Num 1)
                                                     (Num 1))
                                           (GreaterThan (Add (Num 1)
                                                             (Num 10))
                                                        (Num 2))))
  assert(Right 123 == evalNum (StringToNum (Concat (String "12") (String "3"))))
  assert(Left "cannot parse as Num: hello" == evalNum (StringToNum (String "hello")))

What am I missing?

It depends what you want to do with it. If you want to be able to add and equate without worrying about which type of expression you are in, you need to wrap a bit more machinery around your code. You also lose the genericism that I can switch Int and Text out for Decimal and [Party] without writing terribly much code.

Hi Guys. Thank you for both your suggestions.

@bernhard, I think your solution is what I described at the end of my OP. The disadvantage is that the interpreter is partial - i.e. it throws errors during runtime. You also lose the type safety (consider the example I gave at the end) during compile time.

@Gary_Verhaegen I think your suggestion works, however, as you pointed out, I loose the type parameter, which is something I’d like to keep.

I think that at a very fundamental level, the only way to encode this is using functions (which don’t serialize) , or some language construct that allows us to encode the dependency of the output type based on the input type.