Tagged is not a Newtype

by @eborden on October 26, 2020

One of Haskell’s features with the highest return on investment is newtype. Every Haskeller starts their journey using type to define aliases. They soon learn that while type is cheap, it provides little benefit for its small investment and often causes more confusion/indirection as a result. Through trial and error, folk knowledge, and pain they learn to avoid it except for specific circumstances. Eventually they learn that newtype is only moderately more boilerplate, exceptionally more beneficial, and becomes cheaper and cheaper to utilize with GHC features like GeneralizedNewtypeDeriving and DerivingVia. This could be the last stop in the journey, the global maximum, but often it is not.

As learners get deeper into the ecosystem, as they explore more GHC extensions, they find Tagged and DataKinds. Together, these artifacts can be used to define a generic mechanism for ad-hoc type differentiation. A newtype without the boilerplate!

Instead of the error prone

power :: Double -> Double -> Double
power work time = work / time

or the boilerplate heavy

newtype Time = Time { unTime :: Double }

newtype Work = Work { unWork :: Double }

newtype Power = Power { unPower :: Double }

power :: Work -> Time -> Power
power work time = Power $ unWork work / unTime time

we can define

-- | defined in Data.Tagged
newtype Tagged k b = Tagged { untag :: b }

power :: Tagged "work" Double -> Tagged "time" Double -> Tagged "power" Double
power work time = Tagged $ untag work / untag time

We use DataKinds to inhabit the phantom type k in Tagged with a Symbol of our choosing. Voila, an ad-hoc newtype.

Type Safety In Passing

This use of Tagged feels type safe. The compiler agrees that our function is very specific, but this type safety only gets reaped when we pass Tagged values between functions.

We experience type safety here:

allThePower :: [(Tagged "time" Double, Tagged "work" Double)] -> Tagged "power" Double
allThePower = foldl' (+) (Tagged 0) . fmap (uncurry power)

-- error:
--     • Couldn't match type ‘"time"’ with ‘"work"’
--       Expected type: [(Tagged "time" Double, Tagged "work" Double)]
--                      -> Tagged "power" Double
--         Actual type: [(Tagged "work" Double, Tagged "time" Double)]
--                      -> Tagged "power" Double
--     • In the expression: foldl' (+) (Tagged 0) . fmap (uncurry power)
--       In an equation for ‘allThePower’:
--           allThePower = foldl' (+) (Tagged 0) . fmap (uncurry power)
--    |
--    | allThePower = foldl' (+) (Tagged 0) . fmap (uncurry power)
--    |               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Yet, directly calling power has little benefit and treats us to a flavor of dynamic typing that can have consequences.

λ> let time = Tagged 22
λ> let work = Tagged 0

λ> power work time
Tagged 0.0

λ> power time work
Tagged Infinity

With a domain specific newtype GHC can help us.

λ> let time = Time 22
λ> let work = Work 0

λ> power work time
Power 0.0

λ> power time work
-- error:
--     • Couldn't match expected type ‘Work’ with actual type ‘Time’
--     • In the first argument of ‘power’, namely ‘time’
--       In the expression: power time work
--       In an equation for ‘it’: it = power time work

-- error:
--     • Couldn't match expected type ‘Time’ with actual type ‘Work’
--     • In the second argument of ‘power’, namely ‘work’
--       In the expression: power time work
--       In an equation for ‘it’: it = power time work

Furthermore, unwrapping our Tagged values also quivers with dynamism and easily falls prey to simple transposition errors that can arise during initial writing or refactoring.

-- Can you spot the error? GHC can't.
power :: Tagged "work" Double -> Tagged "time" Double -> Tagged "power" Double
power time work = Tagged $ untag work / untag time

If we don’t want type safety to dissolve at the boundary and the terminal point of use, we can gradually increase safety. Using TypeApplications we call our function more explicitly. At that point we have eclipsed the boilerplate of newtype and littered our code with noise.

power :: Tagged "work" Double -> Tagged "time" Double -> Tagged "power" Double
power time work = Tagged @"power" $ untag @"work" work / untag @"time" time
-- error:
--     • Couldn't match type ‘"time"’ with ‘"work"’
--       Expected type: Tagged "work" Double
--         Actual type: Tagged "time" Double
--     • In the second argument of ‘untag’, namely ‘work’
--       In the first argument of ‘(/)`’, namely ‘untag @"work" work’
--       In the second argument of ‘($)’, namely
--         ‘untag @"work" work / untag @"time" time’
--   |
--   | power time work = Tagged @"power" $ untag @"work" work / untag @"time" time
--   |                                                   ^^^^
--
-- error:
--     • Couldn't match type ‘"work"’ with ‘"time"’
--       Expected type: Tagged "time" Double
--         Actual type: Tagged "work" Double
--     • In the second argument of ‘untag’, namely ‘time’
--       In the second argument of ‘(/)’, namely ‘untag @"time" time’
--       In the second argument of ‘($)’, namely
--         ‘untag @"work" work / untag @"time" time’
--   |
--   | power time work = Tagged @"power" $ untag @"work" work / untag @"time" time
--   |                                                                        ^^^^
λ> power (Tagged @"time" 3) (Tagged @"work" 37)
-- error:
--     • Couldn't match type ‘"time"’ with ‘"work"’
--       Expected type: Tagged "work" Double
--         Actual type: Tagged "time" Double
--     • In the first argument of ‘power’, namely ‘(Tagged @"time" 3)’
--       In the expression: power (Tagged @"time" 3) (Tagged @"work" 37)
--       In an equation for ‘it’:
--           it = power (Tagged @"time" 3) (Tagged @"work" 37)

-- error:
--     • Couldn't match type ‘"work"’ with ‘"time"’
--       Expected type: Tagged "time" Double
--         Actual type: Tagged "work" Double
--     • In the second argument of ‘power’, namely ‘(Tagged @"work" 37)’
--       In the expression: power (Tagged @"time" 3) (Tagged @"work" 37)
--       In an equation for ‘it’:
--           it = power (Tagged @"time" 3) (Tagged @"work" 37)

We have pushed type safety to an edge, but is that edge sufficient? Is it worth it? Have we gained more than we invested?

The Ghosts of Departed Opportunities

“Parse don’t validate”, “push constraints upstream”, “the ghosts of departed proofs”, whatever your favored slogan, using Tagged as an ad-hoc newtype doesn’t provide it. Used in this way it is a shotgun loaded by lack of parsing, lack of validation, lack of domain encoding. This use of Tagged as an ad-hoc newtype is a missed opportunity to define a domain concept, ensure invariants via a smart constructor, tune boundary type class instances like FromJSON, and communicate more effectively with your collaborators.

Programming is both the process of automation and the encoding of assumptions. newtypes allow us to encode, isolate, and refine assumptions. Ad-hoc newtyping through Tagged empowers us to litter those assumptions throughout the codebase so they can haunt us forever.

A Poor Man’s Named Argument

Sometimes your arguments truly are ad-hoc, ephemeral, and one-off. Tagged in this circumstance ends up just being a poor replacement for named arguments or a better record system. In a language with anonymous records we’d be far better off.

power :: {work :: Double, time :: Double} -> Double
power {work, time} = work / time

λ> power {work = 3, time = 37}
111

This still suffers from all the caveats that arise from vague domain concepts, but it is concise, easy to use, less error prone, does not have positional semantics, and provides an attractive cost/benefit.

What is Tagged for?

Tagged has a very specific, niche, use. It is the logical extension of Proxy. Where Proxy is a nullary constructor witness for a type, Tagged is a unary constructor value “tagged” with a type witness. When is this useful? Rarely.

data    Proxy  k   = Proxy

newtype Tagged k b = Tagged b