Skip to content

Instantly share code, notes, and snippets.

@hikari-no-yume
Last active August 29, 2015 14:19
Show Gist options
  • Save hikari-no-yume/ea5c08a6c035b836eb55 to your computer and use it in GitHub Desktop.
Save hikari-no-yume/ea5c08a6c035b836eb55 to your computer and use it in GitHub Desktop.
a Haskell translation of a Minima program
--based on Ms. Hale's hastebin of Minima here: http://hastebin.com/ugopowunoy
--see: https://twitter.com/velartrill/status/591072530548535297
--her comments are preceded by "-- "
--mine are preceded by "--"
-- a sketch of the Minima language
--- - - - - - - - - - - - - - - -
-- first off, we should define a unit type
--renamed from "~"
data Foo = Foo
-- booleans are simple enough to implement
--renamed from "bool", "true", "false"
--gotta add "deriving (Eq)" so Haskell lets us compare 'em
--gotta add "deriving (Show)" so Haskell lets us print 'em
data Boo = Troo | Fals deriving (Eq, Show)
-- integers are harder. there are a number of ways to do it
-- but let's do something really evil and encode them in unary
--renamed from "int", "zero", "succ"
--gotta add "deriving (Eq)" so Haskell lets us compare 'em
data Mint = Zero | Succ Mint deriving (Eq)
-- zero = 0; [succ null] = 1; [succ [succ null]] = 2, etc.
-- i really hate the OCamlism here of "constructors as functions"
-- but let's go with it for now
--So it turns out Haskell doesn't support "non-linear patterns" for simplicity
--http://stackoverflow.com/a/1179394/736162
--So we can't do this:
--eq :: a -> a -> Boo
--eq a a = Troo
--eq _ _ = Fals
--And have to do this:
eq :: (Eq a) => a -> a -> Boo
eq a b
| a == b = Troo
| otherwise = Fals
--renamed from "not"
nicht :: Boo -> Boo
nicht Troo = Fals
nicht Fals = Troo
--neq :: a -> a -> Boo
neq :: (Eq a) => a -> a -> Boo
neq a b = nicht (eq a b)
or :: Boo -> Boo -> Boo
or Troo _ = Troo
or _ Troo = Troo
or _ _ = Troo
and :: Boo -> Boo -> Boo
and Troo Troo = Troo
and _ _ = Fals
-- unary increment is simple enough
inc :: Mint -> Mint
inc i = Succ i
-- i'm having a very hard time believing
-- unary addition is actually this easy;
-- my dyscalculic brain is probably
-- lying to me
add :: Mint -> Mint -> Mint
add Zero i = i
add i Zero = i;
add i (Succ x) = Succ (add i x)
-- seq allows throwing away a value, which allows
-- sequencing effectful operations.
seq :: a -> b -> b
seq a b = b
isThree :: Mint -> Boo
isThree x = eq x $ Succ $ Succ $ Succ $ Zero
--lol
--main ~ → !;
--main ~ = ~; *nothing b/c there's nothing with side effects yet, oops
main :: IO ()
main = do
putStrLn $ show $ isThree $ inc $ inc $ inc $ Zero
-- notes:
-- - like in ocaml, 'a marks a generic type bound to "'a"
-- - ! means "diverging;" once this function finishes, the program
-- will terminate. unifies with all types.
-- - main must be a diverging function.
-- - i have NO IDEA what the semantics for the main function should be or even if a main fn makes sense in this context.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment