From a2fe18d004519033251861f229ac5edeb284bc00 Mon Sep 17 00:00:00 2001 From: techieAgnostic Date: Fri, 5 Jul 2019 17:55:48 +1200 Subject: [PATCH] what have I done --- README | 97 +++++++++++++++++++++++++++++ boom.hs | 216 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 313 insertions(+) create mode 100644 README create mode 100644 boom.hs diff --git a/README b/README new file mode 100644 index 0000000..573365c --- /dev/null +++ b/README @@ -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))))))))))))))))))))))))) +``` diff --git a/boom.hs b/boom.hs new file mode 100644 index 0000000..858856f --- /dev/null +++ b/boom.hs @@ -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> + +-}