# Encoding inequalities in an ADT

**URL:** <https://forum.canton.network/t/encoding-inequalities-in-an-adt/1620>\
**Category:** App Development\
**Tags:** daml\
**Created:** [November 11, 2020, 8:35am UTC](https://forum.canton.network/t/encoding-inequalities-in-an-adt/1620 "2020-11-11T08:35:54Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![Luciano](https://yyz2.discourse-cdn.com/flex034/user_avatar/forum.canton.network/luciano/32/319_2.png) [@Luciano](https://forum.canton.network/u/Luciano)\
**Post date:** [November 11, 2020, 8:35am UTC](https://forum.canton.network/t/encoding-inequalities-in-an-adt/1620/1 "2020-11-11T08:35:54Z")

</div>

I have a typeclass that looks like this:

```haskell
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:

```haskell
(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?](https://discuss.daml.com/t/functions-can-we-pass-them-as-arguments-in-a-choice/160/2) , of encoding it as a data type `Obs`:

```haskell
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](https://en.wikibooks.org/wiki/Haskell/GADT#Extending_the_language). 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](http://www.haskellforall.com/2012/06/gadts.html), 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:

```haskell
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

```haskell
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?

---

<div class="post-metadata">

**Author:** ![Gary\_Verhaegen](https://yyz2.discourse-cdn.com/flex034/user_avatar/forum.canton.network/gary_verhaegen/32/81_2.png) [@Gary\_Verhaegen](https://forum.canton.network/u/Gary_Verhaegen)\
**Post date:** [November 11, 2020, 11:26am UTC](https://forum.canton.network/t/encoding-inequalities-in-an-adt/1620/2 "2020-11-11T11:26:53Z")

</div>

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).

```haskell
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))))

```

---

<div class="post-metadata">

**Author:** ![bernhard](https://yyz2.discourse-cdn.com/flex034/user_avatar/forum.canton.network/bernhard/32/356_2.png) [@bernhard](https://forum.canton.network/u/bernhard)\
**Post date:** [November 11, 2020, 1:32pm UTC](https://forum.canton.network/t/encoding-inequalities-in-an-adt/1620/3 "2020-11-11T13:32:44Z")

</div>

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

```haskell
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)

```

---

<div class="post-metadata">

**Author:** ![Gary\_Verhaegen](https://yyz2.discourse-cdn.com/flex034/user_avatar/forum.canton.network/gary_verhaegen/32/81_2.png) [@Gary\_Verhaegen](https://forum.canton.network/u/Gary_Verhaegen)\
**Post date:** [November 12, 2020, 12:01pm UTC](https://forum.canton.network/t/encoding-inequalities-in-an-adt/1620/4 "2020-11-12T12:01:03Z")

</div>

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.

```haskell
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?

---

<div class="post-metadata">

**Author:** ![bernhard](https://yyz2.discourse-cdn.com/flex034/user_avatar/forum.canton.network/bernhard/32/356_2.png) [@bernhard](https://forum.canton.network/u/bernhard)\
**Post date:** [November 12, 2020, 12:10pm UTC](https://forum.canton.network/t/encoding-inequalities-in-an-adt/1620/5 "2020-11-12T12:10:17Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![Luciano](https://yyz2.discourse-cdn.com/flex034/user_avatar/forum.canton.network/luciano/32/319_2.png) [@Luciano](https://forum.canton.network/u/Luciano)\
**Post date:** [November 16, 2020, 7:26am UTC](https://forum.canton.network/t/encoding-inequalities-in-an-adt/1620/6 "2020-11-16T07:26:44Z")

</div>

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.