# Interpreted arithmetic

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


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

• Are language extensions free? If so which ones? – Potato44 Jun 10 '18 at 13:15
• @Potato44 Oh yeah. All language extensions are free. – Wheat Wizard Jun 10 '18 at 13:23
• Heh... This post seems meme-y even though it's not. – Magic Octopus Urn Jun 12 '18 at 18:01

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

• If you swap the equations, you can replace Zero by z. – Ørjan Johansen Jun 10 '18 at 20:28
• @ØrjanJohansen Done. I save 9 bytes for someone and 9 bytes is saved for me. – Potato44 Jun 10 '18 at 23:14
• I don't know how to use type families, but maybe a function like this so you don't need to define + is useful? – Lynn Jun 11 '18 at 9:42
• @Lynn that ends up coming out longer. TIO – Potato44 Jun 11 '18 at 10:53
• @WheatWizard I just realized that the code I posted in the comment because it came out longer is essentially the tail recursive version of your answer. – Potato44 Nov 25 at 1:13

# 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!

• You don't need to count your data declarations to your byte total. I'LL make this clearer in the question when I get a chance – Wheat Wizard Jun 10 '18 at 15:52
• Also I think you can use a general f instead of Succ. – Wheat Wizard Jun 10 '18 at 15:53
• You can save 9 bytes by ditching the colons. – Potato44 Jun 10 '18 at 18:51
• I think Hat Wizard also saved 9, not 6. There were three occurrences of Succ. – Potato44 Jun 10 '18 at 23:20

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

• Nice, I see that your type family is mathematically implementing a*b+c. Is that mention of "division" meant to be "addition"? – Potato44 Nov 24 at 11:23
• btw, you happen to be violating your own spec at the moment. "implement a class that multiplies two Peano numerals" What you have currently isn't a class, it does happen to be of kind Constraint though. So you should either update the spec or revert back to the form that uses a class instead of a type synonym. If I were to use the type synonym I could get my answer down to 96 bytes, so it saves me one more byte than you – Potato44 Nov 24 at 11:36
• @Potato44 I was under the impression that a class was just something with a kind that results in a contraint. Perhaps that was due to a lack of clarity in the question. I will revert back to my 115 answer then. – Wheat Wizard Nov 24 at 14:52