Interpreted arithmetic

Question

A little known fact is that if you turn on enough language extensions (ghc) Haskell becomes a dynamically typed interpreted language! For example the following program implements addition.

{-# Language MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}

data Zero
data Succ a

class Add a b c | a b -> c
instance Add Zero a a
instance (Add a b c) => Add (Succ a) b (Succ c)

This doesn't really look like Haskell any more. For one instead of operating over objects, we operate over types. Each number is it's own type. Instead of functions we have type classes. The functional dependencies allows us to use them as functions between types.

So how do we invoke our code? We use another class

class Test a | -> a
 where test :: a
instance (Add (Succ (Succ (Succ (Succ Zero)))) (Succ (Succ (Succ Zero))) a)
  => Test a

This sets the type of test to the type 4 + 3. If we open this up in ghci we will find that test is indeed of type 7:

Ok, one module loaded.
*Main> :t test
test :: Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))

---

Task

I want you to implement a class that multiplies two Peano numerals (non-negative integers). The Peano numerals will be constructed using the same data types in the example above:

data Zero
data Succ a

And your class will be evaluated in the same way as above as well. You may name your class whatever you wish.

You may use any ghc language extensions you want at no cost to bytes.

Test Cases

These test cases assume your class is named M, you can name it something else if you would like.

class Test1 a| ->a where test1::a
instance (M (Succ (Succ (Succ (Succ Zero)))) (Succ (Succ (Succ Zero))) a)=>Test1 a

class Test2 a| ->a where test2::a
instance (M Zero (Succ (Succ Zero)) a)=>Test2 a

class Test3 a| ->a where test3::a
instance (M (Succ (Succ (Succ (Succ Zero)))) (Succ Zero) a)=>Test3 a

class Test4 a| ->a where test4::a
instance (M (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))) (Succ (Succ (Succ Zero))) a)=>Test4 a

---

Results

*Main> :t test1
test1
  :: Succ
       (Succ
          (Succ
             (Succ
                (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))
*Main> :t test2
test2 :: Zero
*Main> :t test3
test3 :: Succ (Succ (Succ (Succ Zero)))
*Main> :t test4
test4
  :: Succ
       (Succ
          (Succ
             (Succ
                (Succ
                   (Succ
                      (Succ
                         (Succ
                            (Succ
                               (Succ
                                  (Succ
                                     (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))

Draws inspiration from Typing the technical interview

Answer 1

130 121 bytes

^{-9 bytes thanks to Ørjan Johansen}

type family a+b where s a+b=a+s b;z+b=b
type family a*b where s a*b=a*b+b;z*b=z
class(a#b)c|a b->c
instance a*b~c=>(a#b)c

Try it online!

This defines closed type families for addition (+) and multiplication (*). Then a type class (#) is defined that uses the (*) type family along with an equality constraint to convert from the world of type familes to the world of typeclass prolog.

Answer 2

139 bytes

class(a+b)c|a b->c;instance(Zero+a)a;instance(a+b)c=>(s a+b)(s c)
class(a*b)c|a b->c;instance(Zero*a)Zero;instance((a*b)c,(b+c)d)=>(s a*b)d

Try it online!

Defines a type operator *. Equivalent to the Prolog program:

plus(0, A, A).
plus(s(A), B, s(C)) :- plus(A, B, C).
mult(0, _, 0).
mult(s(A), B, D) :- mult(A, B, C), plus(B, C, D).

Potato44 and Hat Wizard saved 9 bytes each. Thanks!

Answer 3

Family-Version, 115 bytes

type family(a%b)c where(a%b)(s c)=s((a%b)c);(s a%b)z=(a%b)b;(z%b)z=z
class(a#b)c|a b->c
instance(a%b)Zero~c=>(a#b)c

Try it online!

This is uses a closed type family like potato44's. Except unlike the other answer I use only 1 type family.

type family(a%b)c where
  -- If the accumulator is Succ c:
  -- the answer is Succ of the answer if the accumulator were c
  (a%b)(s c)=s((a%b)c)
  -- If the left hand argument is Succ a, and the right hand is b
  -- the result is the result if the left were a and the accumulator were b
  (s a%b)z=(a%b)b
  -- If the left hand argument is zero
  -- the result is zero
  (z%b)z=z

This defines an operator on three types. It essentially implements (a*b)+c. Whenever we want to add our right hand argument to the total we instead put it in the accumulator.

This prevents us from needing to define (+) at all. Technically you can use this family to implement addition by doing

class Add a b c | a b -> c
instance (Succ Zero % a) b ~ c => Add a b c

Class-Version, 137 bytes

class(a#b)c d|a b c->d
instance(a#b)c d=>(a#b)(f c)(f d)
instance(a#b)b d=>(f a#b)Zero d
instance(Zero#a)Zero Zero
type(a*b)c=(a#b)Zero c

Try it online!

This class version loses some ground to the family version, however it is still shorter than the shortest class version here. It uses the same approach as my family version.