Variadic number functions

Main.hs

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

------------------------------
-- PROBAT

main :: IO ()
main = mapM_ print
  [ i               -- UNUS (1)
  , i v             -- QUATTUOR (4)
  , m c m x c i i i -- ANNUS NATALIS (1993)
  , m + m x + x     -- COMPUTUS (2020)
  ]

------------------------------
-- LINGUA

i :: Numerus x
i = prorsus 1

v :: Numerus x
v = prorsus 5

x :: Numerus x
x = prorsus 10

l :: Numerus x
l = prorsus 50

c :: Numerus x
c = prorsus 100

d :: Numerus x
d = prorsus 500

m :: Numerus x
m = prorsus 1000

------------------------------
-- CALCULUS

-- A number that can be used either as a constant or as a function that
-- accumulates a total.
type Numerus x = forall k. Numeral x k => k

-- A Roman numeral is a representation of a number. It is either a constant
-- value (such as @i = prorsus 1@) or a function (such as the @v@ in @v i@),
-- and the call site determines which will be used. If we don't explicitly see
-- the numeral in a function position, the @INCOHERENT@ pragma will let GHC
-- default to the first case, which means we can write things like @print i@
-- without having to add annotations.
class Num x => Numeral x k | k -> x where
  prorsus :: x -> k

-- If the numeral (such as @prorsus 1@) is being used as a function, we'll
-- assume it isn't a constant, and start calculating the value using the @Sum@
-- class.
instance (x ~ y, Ord x, Sum x (y -> k)) => Numeral x (y -> k) where
  prorsus = summa 0

-- If the numeral isn't being used as a function, we'll assume it's a numeric
-- constant. We don't actually care /what/ the type is, as long as there's a
-- @Num@ instance. This means our numerals are not limited merely to regular,
-- primitive integers.
instance {-# INCOHERENT #-} (Num x, k ~ x) => Numeral x k where
  prorsus = id




-- Once we've established that we're not just dealing with a constant, we need
-- to read in a sequence of numerals and calculate the total in our desired
-- @Num@ type. To do this, we carry an accumulator (shown in the @summa@
-- signature as @x@).
class Num x => Sum x k | k -> x where
  summa :: x -> k

-- If we have more than one numeral, we read in the first two. If the first is
-- /smaller/ (such as in @ix@), we subtract it from the accumulator. Otherwise,
-- we add it to the accumulator. That's it! For each numeral, we look ahead one
-- place, and perform this action until we've consumed all the numerals.
--
-- The @k@ parameter here means we end up with a variadic function: it takes
-- any number of arguments, as long as they can all be unified to the same
-- @Num@ type.
instance (x ~ y, y ~ z, Ord x, Sum x (z -> k)) => Sum x (y -> z -> k) where
  summa acc x y
    | x < y = summa (acc - x) y
    | otherwise = summa (acc + x) y

-- If the above instance /doesn't/ match, it means we only have one numeral
-- left! At this point, we just add its value to the total, and we're done!
instance {-# INCOHERENT #-} (Num x, k ~ (x -> x)) => Sum x k where
  summa = (+)