haskelltype-systemsphantom-types

Is using Proxy for providing Show instance to a type modeling a physical quantity with multiple units objectively superior to this simpler solution?


I'm reading Haskell in Depth, and I'm at Chapter 11, Type system advances, where a solution (first of at least two) is built for the task of providing a Show instance for a datatype that represents temperature with associated unit.

Now, since more than one solution is presented, I understand that the first one I'm referring to is surely not intended as the definitive silver bullet, but I'd like some help in comparing it with a "dumber" solution I can come up with; some help in understanding whether


The task is to distinguish Celsius and Fahrenheit degrees, and the first proposed solution (built across a few pages) is to define a parametric type for temperatures, to be parametrized with phantom types, which presumably makes using and printing temperatures easier:

newtype Temp unit = Temp Double deriving (Num, Fractional)

data F
data C

class UnitName u where
  unitName :: Proxy u -> String

instance UnitName F where
  unitName :: Proxy F -> String
  unitName _ = "F"

instance UnitName C where
  unitName :: Proxy C -> String
  unitName _ = "C"

instance UnitName u => Show (Temp u) where
  show (Temp t) = show t ++ "°" ++ unitName (Proxy :: Proxy u)

unit :: forall u. UnitName u => Temp u -> String
unit _ = unitName (Proxy :: Proxy u)

-- Incidentally, there's also this, but I don't quite understand what benefit to I get from it.
-- Sure, it allows me to write
-- > unitName (Proxy :: Proxy (Temp C))
-- but why would I do so, if I can just type
-- > unitName (Proxy :: Proxy C)
-- ??
instance UnitName u => UnitName (Temp u) where
  unitName _ = unitName (Proxy :: Proxy u)

Whereas, starting with the sole assumption that we

don't want to define separate data types to store and process the corresponding temperatures¹

I'd have probably accepted the first few lines

newtype Temp unit = Temp Double
  deriving (Num, Fractional)

data F
data C

and then I'd have gone for something more basic:

instance Show F where
  show _ = "F"

instance Show C where
  show _ = "C"

instance Show (Temp F) where
  show (Temp t) = show t ++ "°" ++ show (undefined :: F)

instance Show (Temp C) where
  show (Temp t) = show t ++ "°" ++ show (undefined :: C)

This solution does seem a bit more a hack to me, as I'm really writing undefined here and there, but that seems to me just like a way of turning the phantom types F and C into a Proxy-like type, where the one value is undefined, which creates no issues because it's not evaluated anyway thanks to us passing _ as the parameter to unitName's definitions.

Is this "simpler" solution just uglier, or is it really less usable?


(¹) At this point the author doesn't really explain why. Intuitively I can tell that defining separate data types like this

newtype TempF = TempF Double deriving (Num, Fractional)
newtype TempC = TempC Double deriving (Num, Fractional)

would not allow a generic halding of temperatures at all, whereas the proposed solution does. But it's not like I forsee how deep this advantage is.


Solution

  • No, this should not be done with proxies in modern Haskell, but certainly not with undefined!

    First, it doesn't really make sense at all to distinguish different units for the same physical quantity at the type level. Conceptually a temperature in Celsius and a temperature in Fahrenheit are just different "views" into the same thing; it's for most purposes better to express this by having only a single type for temperature whose numerical representation is hidden, and then exporting optics or pattern synonyms for the different units. That's an topic kind of tangential to the question though.

    Another tangent: Show instances shouldn't generate strings like 5°C, as that is not valid Haskell code.

    However, if we accept the premise of the example, this is how I would code it:

    {-# LANGUAGE AllowAmbiguousTypes, TypeApplications, ScopedTypeVariables, UnicodeSyntax #-}
    
    class UnitName u where
      unitName :: String
    
    instance UnitName F where
      unitName = "F"
    instance UnitName C where
      unitName = "C"
    
    instance ∀ u . UnitName u => Show (Temp u) where
      show (Temp t) = show t ++ "°" ++ unitName @u
    

    As you see, TypeApplications makes it quite unnecessary to fiddle with either proxies or undefined.

    An alternative that could be considered is to just use type-level strings for the unit, instead of ad-hoc defined types.

    {-# LANGUAGE DataKinds, KindSignatures #-}
    
    import GHC.TypeLits (Symbol, KnownSymbol, SymbolVal)
    
    newtype Temp (unit :: Symbol) = Temp Double
     deriving (Num, Fractional) -- BTw those are a bad idea too
    
    instance ∀ u . KnownSymbol u => Show (Temp u) where
      show (Temp t) = show t ++ "°" ++ symbolVal (Proxy @u)
    

    Here a proxy is required becauses the TypeLits module predates the TypeApplications extension. singletons-base exports the generic demote which uses the modern type application style, but it is a heavy dependency and doesn't really make sense to pull in just to avoid a proxy.

    import Prelude.Singletons (demote)
    import GHC.TypeLits.Singletons ()
    
    instance ∀ u . KnownSymbol u => Show (Temp u) where
      show (Temp t) = show t ++ "°" ++ demote @u
    

    Indeed, the custom unit-types could also be used within the singletons framework, but this leads too far from the question.