what have I done
This commit is contained in:
commit
a2fe18d004
97
README
Normal file
97
README
Normal file
@ -0,0 +1,97 @@
|
||||
# Boom
|
||||
|
||||
**Problem:**
|
||||
Return the numbers 0-n, but replace every number with a '3' as one of the digits with "Boom"
|
||||
|
||||
I did this in the type system because I wanted to piss off my flatmate, who gave me this to try out, but also because I hate myself.
|
||||
|
||||
I cheated a little at the end, because I cbf converting my representation to standard Church Encoding, so everything is a list of digits instead of a number.
|
||||
|
||||
## Running
|
||||
|
||||
start up `ghci` and type:
|
||||
|
||||
```
|
||||
:t solution (nil :: X)
|
||||
```
|
||||
|
||||
where X is a church encoding using S as the successor function, and Z as the atom.
|
||||
|
||||
## Example
|
||||
|
||||
```
|
||||
:t solution (nil :: (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))
|
||||
```
|
||||
|
||||
will return (formatted to save your eyes):
|
||||
|
||||
```
|
||||
solution (nil :: (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))
|
||||
:: Cons
|
||||
(Cons Z Nil)
|
||||
(Cons
|
||||
(Cons (S Z) Nil)
|
||||
(Cons
|
||||
(Cons (S (S Z)) Nil)
|
||||
(Cons
|
||||
Boom
|
||||
(Cons
|
||||
(Cons (S (S (S (S Z)))) Nil)
|
||||
(Cons
|
||||
(Cons (S (S (S (S (S Z))))) Nil)
|
||||
(Cons
|
||||
(Cons (S (S (S (S (S (S Z)))))) Nil)
|
||||
(Cons
|
||||
(Cons (S (S (S (S (S (S (S Z))))))) Nil)
|
||||
(Cons
|
||||
(Cons (S (S (S (S (S (S (S (S Z)))))))) Nil)
|
||||
(Cons
|
||||
(Cons (S (S (S (S (S (S (S (S (S Z))))))))) Nil)
|
||||
(Cons
|
||||
(Cons (S Z)
|
||||
(Cons Z Nil))
|
||||
(Cons
|
||||
(Cons (S Z)
|
||||
(Cons (S Z) Nil))
|
||||
(Cons
|
||||
(Cons (S Z)
|
||||
(Cons (S (S Z)) Nil))
|
||||
(Cons
|
||||
Boom
|
||||
(Cons
|
||||
(Cons (S Z)
|
||||
(Cons (S (S (S (S Z)))) Nil))
|
||||
(Cons
|
||||
(Cons (S Z)
|
||||
(Cons (S (S (S (S (S Z))))) Nil))
|
||||
(Cons
|
||||
(Cons (S Z)
|
||||
(Cons (S (S (S (S (S (S Z)))))) Nil))
|
||||
(Cons
|
||||
(Cons (S Z)
|
||||
(Cons (S (S (S (S (S (S (S Z))))))) Nil))
|
||||
(Cons
|
||||
(Cons (S Z)
|
||||
(Cons (S (S (S (S (S (S (S (S Z)))))))) Nil))
|
||||
(Cons
|
||||
(Cons (S Z)
|
||||
(Cons (S (S (S (S (S (S (S (S (S Z))))))))) Nil))
|
||||
(Cons
|
||||
(Cons (S (S Z))
|
||||
(Cons Z Nil))
|
||||
(Cons
|
||||
(Cons (S (S Z))
|
||||
(Cons (S Z) Nil))
|
||||
(Cons
|
||||
(Cons (S (S Z))
|
||||
(Cons (S (S Z)) Nil))
|
||||
(Cons
|
||||
Boom
|
||||
(Cons
|
||||
(Cons (S (S Z))
|
||||
(Cons (S (S (S (S Z)))) Nil))
|
||||
(Cons
|
||||
(Cons (S (S Z))
|
||||
(Cons (S (S (S (S (S Z))))) Nil))
|
||||
Nil)))))))))))))))))))))))))
|
||||
```
|
||||
216
boom.hs
Normal file
216
boom.hs
Normal file
@ -0,0 +1,216 @@
|
||||
{-# OPTIONS_GHC -fno-warn-missing-methods #-}
|
||||
{-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE FunctionalDependencies #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
|
||||
class Solution n r | n -> r
|
||||
where solution :: n -> r
|
||||
instance (InitList n l, Map BoomOrNum' l r)
|
||||
=> Solution n r where solution = nil
|
||||
|
||||
data BoomOrNum'
|
||||
|
||||
nil = undefined
|
||||
|
||||
class EqNine d b | d -> b
|
||||
instance (Equal d (S (S (S (S (S (S (S (S (S Z))))))))) r)
|
||||
=> EqNine d r
|
||||
|
||||
class Inc l r | l -> r
|
||||
instance (Reverse Nil l nl, Inc' True nl nr, Reverse Nil nr r)
|
||||
=> Inc l r
|
||||
|
||||
class Inc1 b n r | b n -> r
|
||||
instance Inc1 True d Z
|
||||
instance (Add (S Z) d r)
|
||||
=> Inc1 False d r
|
||||
|
||||
class Inc' c l r | c l -> r
|
||||
instance Inc' False l l
|
||||
instance Inc' True Nil (Cons (S Z) Nil)
|
||||
instance (Inc1 nc x nx, EqNine x nc, Inc' nc xs r)
|
||||
=> Inc' True (Cons x xs) (Cons nx r)
|
||||
|
||||
class InitList' t n l a | t n l -> a
|
||||
instance InitList' Z n l (Cons n l)
|
||||
instance (Inc n nn, InitList' x nn (Cons n l) a)
|
||||
=> InitList' (S x) n l a
|
||||
|
||||
class InitList t l | t -> l
|
||||
instance (InitList' t (Cons Z Nil) Nil a, Reverse Nil a l)
|
||||
=> InitList t l
|
||||
|
||||
data Boom
|
||||
|
||||
class EqualThree x r | x -> r
|
||||
instance (Equal x (S (S (S Z))) a)
|
||||
=> EqualThree x a
|
||||
|
||||
data EqualThree'
|
||||
|
||||
class Apply f a r | f a -> r
|
||||
instance (EqualThree x r)
|
||||
=> Apply EqualThree' x r
|
||||
instance (BoomOrNum x r)
|
||||
=> Apply BoomOrNum' x r
|
||||
|
||||
class Map f xs ys | f xs -> ys
|
||||
instance Map f Nil Nil
|
||||
instance (Apply f x y, Map f xs ys)
|
||||
=> Map f (Cons x xs) (Cons y ys)
|
||||
|
||||
class Boom' c n r | c n -> r
|
||||
instance Boom' True n Boom
|
||||
instance Boom' False n n
|
||||
|
||||
class BoomOrNum n r | n -> r
|
||||
instance (Map EqualThree' n bs, AnyTrue bs a, Boom' a n r)
|
||||
=> BoomOrNum n r
|
||||
|
||||
data Nil
|
||||
data Cons x xs
|
||||
|
||||
class First list x | list -> x
|
||||
instance First Nil Nil
|
||||
instance First (Cons x more) x
|
||||
|
||||
class ListConcat a b c | a b -> c
|
||||
instance ListConcat Nil x x
|
||||
instance (ListConcat as bs cs)
|
||||
=> ListConcat (Cons a as) bs (Cons a cs)
|
||||
|
||||
class ListConcatAll ls l | ls -> l
|
||||
instance ListConcatAll Nil Nil
|
||||
instance (ListConcat chunk acc result,
|
||||
ListConcatAll rest acc)
|
||||
=> ListConcatAll (Cons chunk rest) result
|
||||
|
||||
class AnyTrue list t | list -> t
|
||||
instance AnyTrue Nil False
|
||||
instance AnyTrue (Cons True more) True
|
||||
instance (AnyTrue list t)
|
||||
=> AnyTrue (Cons False list) t
|
||||
|
||||
data True
|
||||
data False
|
||||
|
||||
class Not b1 b | b1 -> b
|
||||
instance Not False True
|
||||
instance Not True False
|
||||
|
||||
class Or b1 b2 b | b1 b2 -> b
|
||||
instance Or True True True
|
||||
instance Or True False True
|
||||
instance Or False True True
|
||||
instance Or False False False
|
||||
|
||||
data Z
|
||||
data S n
|
||||
|
||||
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 LessThan a b t | a b -> t
|
||||
instance LessThan Z Z False
|
||||
instance LessThan (S x) Z False
|
||||
instance LessThan Z (S x) True
|
||||
instance (LessThan a b t)
|
||||
=> LessThan (S a) (S b) t
|
||||
|
||||
class Add x y z | x y -> z
|
||||
instance Add x Z x
|
||||
instance Add Z y y
|
||||
instance (Add (S x) y z)
|
||||
=> Add x (S y) z
|
||||
|
||||
class Multiply x y a z | x y a -> z
|
||||
instance Multiply Z y a a
|
||||
instance Multiply x Z a a
|
||||
instance (Add x a r, Multiply x y r z)
|
||||
=> Multiply x (S y) a z
|
||||
|
||||
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
|
||||
|
||||
{-
|
||||
|
||||
*Main> :t solution (nil :: (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))
|
||||
solution (nil :: (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))
|
||||
:: Cons
|
||||
(Cons Z Nil)
|
||||
(Cons
|
||||
(Cons (S Z) Nil)
|
||||
(Cons
|
||||
(Cons (S (S Z)) Nil)
|
||||
(Cons
|
||||
Boom
|
||||
(Cons
|
||||
(Cons (S (S (S (S Z)))) Nil)
|
||||
(Cons
|
||||
(Cons (S (S (S (S (S Z))))) Nil)
|
||||
(Cons
|
||||
(Cons (S (S (S (S (S (S Z)))))) Nil)
|
||||
(Cons
|
||||
(Cons (S (S (S (S (S (S (S Z))))))) Nil)
|
||||
(Cons
|
||||
(Cons (S (S (S (S (S (S (S (S Z)))))))) Nil)
|
||||
(Cons
|
||||
(Cons (S (S (S (S (S (S (S (S (S Z))))))))) Nil)
|
||||
(Cons
|
||||
(Cons (S Z)
|
||||
(Cons Z Nil))
|
||||
(Cons
|
||||
(Cons (S Z)
|
||||
(Cons (S Z) Nil))
|
||||
(Cons
|
||||
(Cons (S Z)
|
||||
(Cons (S (S Z)) Nil))
|
||||
(Cons
|
||||
Boom
|
||||
(Cons
|
||||
(Cons (S Z)
|
||||
(Cons (S (S (S (S Z)))) Nil))
|
||||
(Cons
|
||||
(Cons (S Z)
|
||||
(Cons (S (S (S (S (S Z))))) Nil))
|
||||
(Cons
|
||||
(Cons (S Z)
|
||||
(Cons (S (S (S (S (S (S Z)))))) Nil))
|
||||
(Cons
|
||||
(Cons (S Z)
|
||||
(Cons (S (S (S (S (S (S (S Z))))))) Nil))
|
||||
(Cons
|
||||
(Cons (S Z)
|
||||
(Cons (S (S (S (S (S (S (S (S Z)))))))) Nil))
|
||||
(Cons
|
||||
(Cons (S Z)
|
||||
(Cons (S (S (S (S (S (S (S (S (S Z))))))))) Nil))
|
||||
(Cons
|
||||
(Cons (S (S Z))
|
||||
(Cons Z Nil))
|
||||
(Cons
|
||||
(Cons (S (S Z))
|
||||
(Cons (S Z) Nil))
|
||||
(Cons
|
||||
(Cons (S (S Z))
|
||||
(Cons (S (S Z)) Nil))
|
||||
(Cons
|
||||
Boom
|
||||
(Cons
|
||||
(Cons (S (S Z))
|
||||
(Cons (S (S (S (S Z)))) Nil))
|
||||
(Cons
|
||||
(Cons (S (S Z))
|
||||
(Cons (S (S (S (S (S Z))))) Nil))
|
||||
Nil)))))))))))))))))))))))))
|
||||
*Main>
|
||||
|
||||
-}
|
||||
Loading…
Reference in New Issue
Block a user