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.
newtype
s 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