Browse Source

first commit

master
Thorn Avery 4 years ago
commit
6a52aa8da8
2 changed files with 148 additions and 0 deletions
  1. +51
    -0
      README.md
  2. +97
    -0
      collatz.hs

+ 51
- 0
README.md View File

@@ -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 ]
```

+ 97
- 0
collatz.hs View File

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

Loading…
Cancel
Save