From 6a52aa8da8e2bbc8b3057c893a13bbb235d1fb14 Mon Sep 17 00:00:00 2001
From: tA <s@p7.co.nz>
Date: Wed, 17 Jul 2019 14:29:55 +1200
Subject: [PATCH] first commit

---
 README.md  | 51 +++++++++++++++++++++++++++++++++
 collatz.hs | 97 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 148 insertions(+)
 create mode 100644 README.md
 create mode 100644 collatz.hs

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..d50feda
--- /dev/null
+++ b/README.md
@@ -0,0 +1,51 @@
+# Collatz Conjecture
+
+Collatz Conjecture (Snowflake / `3n+1`) done in the GHC Type System.
+
+## Running
+
+in `ghci` load the file:
+
+```
+:load collatz.hs
+```
+
+and run with the following:
+
+```
+:t solution (nil :: X)
+```
+
+where `X` is the church encoding using `S n` and `Z`, ie
+
+`(S (S (S Z)))` is the number `3`
+
+## Example
+
+```
+*Main> :t solution (nil :: (S (S (S Z))))
+solution (nil :: (S (S (S Z))))
+  :: Cons
+       (S (S (S Z)))
+     (Cons
+       (S (S (S (S (S (S (S (S (S (S Z))))))))))
+     (Cons
+       (S (S (S (S (S Z)))))
+     (Cons
+       (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))
+     (Cons
+       (S (S (S (S (S (S (S (S Z))))))))
+     (Cons
+       (S (S (S (S Z))))
+     (Cons
+       (S (S Z))
+     (Cons
+       (S Z)
+     Nil)))))))
+```
+
+which translates to the following list:
+
+```
+[ 3 10 5 16 8 4 2 1 ]
+```
diff --git a/collatz.hs b/collatz.hs
new file mode 100644
index 0000000..37dcca9
--- /dev/null
+++ b/collatz.hs
@@ -0,0 +1,97 @@
+{-# OPTIONS_GHC -fno-warn-missing-methods #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+nil = undefined
+
+data True
+data False
+
+data S n
+data Z
+
+data Nil
+data Cons h t
+
+class Not t b | t -> b
+instance Not True False
+instance Not False True
+
+class And a b r | a b -> r
+instance And True True True
+instance And True False False
+instance And False True False
+instance And False False False
+
+class Equal a b t | a b -> t
+instance Equal Z Z True
+instance Equal (S a) Z False
+instance Equal Z (S b) False
+instance (Equal a b t)
+   => Equal (S a) (S b) t
+
+class Add x y r | x y -> r
+instance Add x Z x
+instance (Add (S x) n r)
+   => Add x (S n) r
+
+class Mul x y a r | x y a -> r
+instance Mul x Z a a
+instance Mul Z y a a
+instance (Add x a n, Mul x y n t)
+   => Mul x (S y) a t
+
+class Half x a r | x a -> r
+instance Half Z a a
+instance Half (S Z) a a
+instance (Half n (S a) r)
+   => Half (S (S n)) a r
+
+class ThreeEnPlusOne x v | x -> v
+instance (Mul (S (S (S Z))) x Z i)
+   => ThreeEnPlusOne x (S i)
+
+class If c t f r | c t f -> r
+instance If True t f t
+instance If False t f f
+
+class EqOne x r | x -> r
+instance (Equal x (S Z) b)
+   => EqOne x b
+
+class IsEven a b | a -> b
+instance IsEven Z True
+instance IsEven (S Z) False
+instance (IsEven n r)
+   => IsEven (S (S n)) r
+
+class IsOdd a b | a -> b
+instance (IsEven a i, Not i r)
+   => IsOdd a r
+
+class Branch b h n | b h -> n
+instance (Half h Z r)
+   => Branch True h r
+instance (ThreeEnPlusOne h r)
+   => Branch False h r
+
+class RunChain b h t r | b h t -> r
+instance RunChain True h xs xs
+instance ( IsEven h e
+         , EqOne h b
+         , Branch e h v
+         , RunChain b v (Cons h t) r
+         )
+   => RunChain False h t r
+
+class Reverse i l r | i l -> r
+instance Reverse i Nil i
+instance (Reverse (Cons x i) xs r)
+   => Reverse i (Cons x xs) r 
+
+class Solution n r | n -> r
+   where solution :: n -> r
+instance (RunChain False n Nil o, Reverse Nil o a)
+   => Solution n a where solution = nil