diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,18 @@ +Copyright Gustavo Roscoe (c) 2019 + +Permission is hereby granted, free of charge, to any person obtaining a copy of +this software and associated documentation files (the "Software"), to deal in +the Software without restriction, including without limitation the rights to +use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of +the Software, and to permit persons to whom the Software is furnished to do so, +subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS +FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR +COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER +IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN +CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,24 @@ +# simple-units +A Haskell library for simple arithmetic with SI units using type-checked dimensional analysis. + +```haskell +>>> let newton = kilogram .* meter ./ (second .* second) +>>> 23*newton +23.0 kg*m/s^2 +>>> let g = 6.67408e-11 * newton .* (meter .* meter) ./ (kilogram .* kilogram) +>>> g -- gravitational constant +6.67408e-11 m^3/kg*s^2 +>>> let gravity m1 m2 r = g .* (m1 * kilogram) .* (m2 * kilogram) ./ (r*meter .* r*meter) +>>> let earth_mass = 5.972e24 * kilogram +>>> let mars_mass = 6.417e23 * kilogram +>>> let earth_radius = 6371e3 * meter +>>> let mars_radius = 3389.5e3 * meter +>>> let weight_on_earth mass = gravity mass earth_mass earth_radius +>>> let weight_on_mars mass = gravity mass mars_mass mars_radius +>>> weight_on_earth (80 * kilogram) +785.5719790179963 kg*m/s^2 +>>> weight_on_mars (80 * kilogram) +298.22370259533704 kg*m/s^2 +>>> weight_on_mars 1 ./ weight_on_earth 1 +0.3796261966575378 +``` diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/simple-units.cabal b/simple-units.cabal new file mode 100644 --- /dev/null +++ b/simple-units.cabal @@ -0,0 +1,44 @@ +cabal-version: 1.12 + +-- This file has been generated from package.yaml by hpack version 0.31.1. +-- +-- see: https://github.com/sol/hpack +-- +-- hash: 1bf2ea2a4041479d0c14336601f236f12e4c746191ab5dff6a13b335a3e29fef + +name: simple-units +version: 1.0.0.0 +synopsis: Simple arithmetic with SI units using type-checked dimensional analysis. +description: Please see the README on GitHub at +category: Numeric, Numerical +homepage: https://github.com/groscoe/simple-units#readme +bug-reports: https://github.com/groscoe/simple-units/issues +author: Gustavo Roscoe +maintainer: gustavo@gustavoroscoe.com +copyright: 2019 Gustavo Roscoe +license: MIT +license-file: LICENSE +build-type: Simple +extra-source-files: + README.md + +source-repository head + type: git + location: https://github.com/groscoe/simple-units + +library + exposed-modules: + Units.Simple + other-modules: + Units.Simple.Arithmetic + Units.Simple.Internals + Units.Simple.Quantity + Units.Simple.Unit + Paths_simple_units + hs-source-dirs: + src + ghc-options: -Wall -Wcompat + build-depends: + base >=4.9 && <5 + , first-class-families >=0.5 && <0.6 + default-language: Haskell2010 diff --git a/src/Units/Simple.hs b/src/Units/Simple.hs new file mode 100644 --- /dev/null +++ b/src/Units/Simple.hs @@ -0,0 +1,115 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE DataKinds #-} +module Units.Simple + (-- *The @Quantity@ type + Quantity () + , fromQuantity + , Unit (..) + , Units + , SingleUnit + , UnitRepr + , showUnits + + -- * Basic arithmetic with quantities + , (.+) + , (.-) + , (.*) + , (./) + + -- *Base SI Units + -- |Smart constructors for quantities in all the base SI Units. + -- The constructors are provided in both unitary (non-ticked) and + -- function (ticked) forms. + -- + -- Examples: + -- + -- >>> 273.0*kelvin -- unitary form + -- 273.0 K + -- >>> kelvin' 273.0 -- function form + -- 273.0 K + , adim + , adim' + , meter + , meter' + , kilogram + , kilogram' + , second + , second' + , ampere + , ampere' + , kelvin + , kelvin' + , mole + , mole' + , candela + , candela' + ) where + + +import Units.Simple.Quantity +import Units.Simple.Arithmetic +import Units.Simple.Unit + +type SingleUnit (u :: Unit) = '( '[ '(u, 1)], '[]) +type Adimensional = '( '[], '[]) + +-- | A quantity with no associated dimension. Can be multiplied or divided +-- by any other quantity, but can only be added to or subtracted from +-- other adimensional quantities. +-- +-- >>> 2*adim + 4*adim +-- 6 +-- >>> adim .+ meter +-- +-- :79:1-13: error: +-- • Unit mismatch: and m +-- • In the expression: adim .+ meter +-- In an equation for ‘it’: it = adim .+ meter +adim :: Num a => Quantity Adimensional a +adim = Quantity 1 + +meter :: Num a => Quantity (SingleUnit 'Meter) a +meter = Quantity 1 + +kilogram :: Num a => Quantity (SingleUnit 'Kilogram) a +kilogram = Quantity 1 + +second :: Num a => Quantity (SingleUnit 'Second) a +second = Quantity 1 + +ampere :: Num a => Quantity (SingleUnit 'Ampere) a +ampere = Quantity 1 + +kelvin :: Num a => Quantity (SingleUnit 'Kelvin) a +kelvin = Quantity 1 + +mole :: Num a => Quantity (SingleUnit 'Mole) a +mole = Quantity 1 + +candela :: Num a => Quantity (SingleUnit 'Candela) a +candela = Quantity 1 + +adim' :: Num a => a -> Quantity Adimensional a +adim' = Quantity + +meter' :: Num a => a -> Quantity (SingleUnit 'Meter) a +meter' = Quantity + +kilogram' :: Num a => a -> Quantity (SingleUnit 'Kilogram) a +kilogram' = Quantity + +second' :: Num a => a -> Quantity (SingleUnit 'Second) a +second' = Quantity + +ampere' :: Num a => a -> Quantity (SingleUnit 'Ampere) a +ampere' = Quantity + +kelvin' :: Num a => a -> Quantity (SingleUnit 'Kelvin) a +kelvin' = Quantity + +mole' :: Num a => a -> Quantity (SingleUnit 'Mole) a +mole' = Quantity + +candela' :: Num a => a -> Quantity (SingleUnit 'Candela) a +candela' = Quantity diff --git a/src/Units/Simple/Arithmetic.hs b/src/Units/Simple/Arithmetic.hs new file mode 100644 --- /dev/null +++ b/src/Units/Simple/Arithmetic.hs @@ -0,0 +1,154 @@ +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +module Units.Simple.Arithmetic + ( (.+) + , (.-) + , (.*) + , (./) + ) where + +import Data.Kind +import GHC.TypeLits as TL + +import Fcf + +import Units.Simple.Unit +import Units.Simple.Quantity +import Units.Simple.Internals (Foldl, DeleteBy, Sort) + + +data Lookup' :: [(k, b)] -> k -> Exp (Maybe b) +type instance Eval (Lookup' as a) = Eval (Lookup a as) + +type InList (as :: [(k, b)]) = IsJust <=< Lookup' as + +type And (f :: a -> Exp Bool) (as :: [a]) = Foldr (&&) 'True (Eval (Map f as)) + +type AllInSecond (l1 :: [(k, a)]) (l2 :: [(k, a)]) = And (InList l2 <=< Fst) l1 + +type SameMaps (l1 :: [(k, a)]) (l2 :: [(k, a)]) = Eval (AllInSecond l1 l2) && Eval (AllInSecond l2 l1) + +type SameUnits' (u1 :: Units) (u2 :: Units) = Eval (SameMaps (Eval (Fst u1)) (Eval (Fst u2))) + && Eval (SameMaps (Eval (Snd u1)) (Eval (Snd u2))) + +type family SameUnits (u1 :: Units) (u2 :: Units) :: Constraint where + SameUnits u1 u2 = If (Eval (SameUnits' u1 u2)) + (Eval (SameUnits' u1 u2) ~ 'True) + (TypeError + ('Text "Unit mismatch: " + ':<>: 'Text (UnitRepr u1) + ':<>: 'Text " and " + ':<>: 'Text (UnitRepr u2))) + +type CleanUnitList = Filter (Not <=< TyEq 0 <=< Snd) +type CleanUnits us = (CleanUnitList *** CleanUnitList) us + +data CancelUnit :: Unit' -> Unit' -> Exp (Unit', Unit') +type instance Eval (CancelUnit '(a, m) '(b, n)) = + If (Eval (LiftM2 (&&) (TyEq a b) (n >= m))) + '( '(a, 0), '(b, n TL.- m)) + '( '(a, m TL.- n), '(b, 0)) + +type GetMatchingUnits l1 l2 = + (Filter (Flip UnitInList l2) *** Filter (Flip UnitInList l1)) =<< (Sort *** Sort) '(l1, l2) +type CancelMatchingUnitLists l1 l2 = + Unzip (Uncurry (ZipWith CancelUnit) (Eval (GetMatchingUnits l1 l2))) +type CancelUnitLists l1 l2 = + ((++) (Eval (l1 \\ l2)) *** (++) (Eval (l2 \\ l1))) =<< CancelMatchingUnitLists l1 l2 +type CancelUnits (a :: Units) = CancelUnitLists (Eval (Fst a)) (Eval (Snd a)) + +data SameUnit :: Unit' -> Unit' -> Exp Bool +type instance Eval (SameUnit a b) = Eval (LiftM2 TyEq (Fst a) (Fst b)) +type (\\) = Foldl (Flip (DeleteBy SameUnit)) + +data MergeUnit :: Unit' -> Unit' -> Exp Unit' +type instance Eval (MergeUnit '(a, m) '(b, n)) = + If (Eval (TyEq a b)) + '(a, (TL.+) m n) + '(b, n) + +data UnitInList :: Unit' -> [Unit'] -> Exp Bool +type instance Eval (UnitInList '(u, n) '[]) = 'False +type instance Eval (UnitInList '(u, n) ('(v, _) ': xs)) = Eval (Eval (TyEq u v) || Eval (UnitInList '(u, n) xs)) + +data MergeUnitFromList :: u -> [us] -> Exp [us] +type instance Eval (MergeUnitFromList u us) = Eval (Map (MergeUnit u) us) + +type MergeUnitLists (us1 :: [Unit']) (us2 :: [Unit']) = Foldr MergeUnitFromList us2 us1 +data MergeUnits' :: Units -> Units -> Exp Units +type instance Eval (MergeUnits' '(num1, denom1) '(num2, denom2)) = + Eval (CancelUnits + '( Eval (Eval (MergeUnitLists num1 num2) ++ Eval (Filter (Not <=< Flip UnitInList num2) num1)) + , Eval (Eval (MergeUnitLists denom1 denom2) ++ Eval (Filter (Not <=< Flip UnitInList denom2) denom1)))) + +type MergeUnits us1 us2 = Eval (CleanUnits (Eval (MergeUnits' us1 us2))) + +data Recip' :: Units -> Exp Units +type instance Eval (Recip' '(num, denom)) = '(denom, num) +type Recip a = Eval (Recip' a) + +-- |Sums two quantities with the same units. Summing quantities with different units +-- results in a type error. +-- +-- Examples: +-- +-- >>> 2*meter .+ 3*meter +-- 5 m +-- >>> 2*meter .+ 1*second +-- +-- :16:1-19: error: +-- • Unit mismatch: m and s +-- • In the expression: 2 * meter .+ 1 * second +-- In an equation for ‘it’: it = 2 * meter .+ 1 * second +(.+) :: (SameUnits u1 u2, Num a) => Quantity u1 a -> Quantity u2 a -> Quantity u1 a +Quantity x .+ Quantity y = Quantity (x + y) +infixl 5 .+ + +-- |Subtracts two quantities with the same units. Subtracting quantities with different units +-- results in a type error. +-- +-- Examples: +-- +-- >>> let newton = kilogram .* meter ./ (second .* second) +-- >>> 10*newton - 2*newton +-- 8.0 kg*m/s^2 +(.-) :: (SameUnits u1 u2, Num a) => Quantity u1 a -> Quantity u2 a -> Quantity u1 a +Quantity x .- Quantity y = Quantity (x - y) +infixl 5 .- + +-- |Multiplies two quantities correctly merging their units. +-- +-- Examples: +-- +-- >>> meter .* meter +-- 1 m^2 +-- >>> let mps = meter ./ second +-- >>> 20*mps .* 60*second +-- 1200.0 m +-- +-- __Important:__ Though @Quantity a@ has a @Num@ instance for convenience, it +-- __must not__ be used for anything other than interacting with literals, otherwise +-- the units will __not__ be correct: +-- +-- >>> 2*meter * 3*meter -- note that (*) was used in place of (.*) +-- 6 m +-- >>> 2*meter .* 3*meter -- this is the correct usage +-- 6 m^2 +(.*) :: Num a => Quantity us1 a -> Quantity us2 a -> Quantity (MergeUnits us1 us2) a +Quantity x .* Quantity y = Quantity (x * y) +infixl 6 .* + +-- | Divides a quantity by another correctly merging their units. +-- +-- Examples: +-- +-- >>> let coulomb = second .* ampere +-- >>> 20*coulomb ./ 2*second +-- 10.0 A +(./) :: Fractional a => Quantity us1 a -> Quantity us2 a -> Quantity (MergeUnits us1 (Recip us2)) a +Quantity x ./ Quantity y = Quantity (x / y) +infixl 6 ./ diff --git a/src/Units/Simple/Internals.hs b/src/Units/Simple/Internals.hs new file mode 100644 --- /dev/null +++ b/src/Units/Simple/Internals.hs @@ -0,0 +1,79 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeFamilies #-} +module Units.Simple.Internals where + +import GHC.TypeLits hiding (type (<=)) +import qualified GHC.TypeLits as TL + +import Fcf hiding (type (<=)) +import qualified Fcf + + +data ApSep :: Symbol -> Symbol -> Symbol -> Exp Symbol +type instance Eval (ApSep sep x xs) = sep `AppendSymbol` x `AppendSymbol` xs + +type Intersperse' sep xs = Foldr (ApSep sep) "" xs + +data Intersperse :: Symbol -> [Symbol] -> Exp Symbol +type instance Eval (Intersperse _ '[]) = "" +type instance Eval (Intersperse sep (x ': xs)) = x `AppendSymbol` Eval (Intersperse' sep xs) + + +data NatToDigit :: Nat -> Exp Symbol +type instance Eval (NatToDigit 0) = "0" +type instance Eval (NatToDigit 1) = "1" +type instance Eval (NatToDigit 2) = "2" +type instance Eval (NatToDigit 3) = "3" +type instance Eval (NatToDigit 4) = "4" +type instance Eval (NatToDigit 5) = "5" +type instance Eval (NatToDigit 6) = "6" +type instance Eval (NatToDigit 7) = "7" +type instance Eval (NatToDigit 8) = "8" +type instance Eval (NatToDigit 9) = "9" + +data (<>) :: Exp a -> Exp a -> Exp a +type instance Eval ((a :: Exp Symbol) <> (b :: Exp Symbol)) = Eval a `AppendSymbol` Eval b + +data (/) :: Nat -> Nat -> Exp Nat +type instance Eval (a / b) = a `TL.Div` b + +data (%) :: Nat -> Nat -> Exp Nat +type instance Eval (a % b) = a `TL.Mod` b + +data Show' :: a -> Exp Symbol +type instance Eval (Show' (n :: Nat)) = Eval (Guarded n + '[ Flip (Fcf.<=) 9 ':= NatToDigit n + , Otherwise ':= Show' (Eval (n / 10)) <> Show' (Eval (n % 10)) + ]) + + +data (<=) :: k -> k -> Exp Bool +type instance Eval ((a :: Nat) <= (b :: Nat)) = a <=? b +type instance Eval ((a :: Symbol) <= (b :: Symbol)) = Eval (Guarded (CmpSymbol a b) + '[ TyEq 'EQ ':= Pure 'True + , TyEq 'LT ':= Pure 'True + , Otherwise ':= Pure 'False + ]) +type instance Eval ('(a, _) <= '(b, _)) = Eval (a <= b) + + +data Sort :: [a] -> Exp [a] +type instance Eval (Sort '[]) = '[] +type instance Eval (Sort (pivot ': rest)) = + Eval (Eval + (Eval (Sort (Eval (Filter (Flip (<=) pivot) rest))) + ++ '[pivot]) + ++ Eval (Sort (Eval (Filter (Not <=< Flip (<=) pivot) rest)))) + +data DeleteBy :: (a -> a-> Exp Bool) -> a -> [a] -> Exp [a] +type instance Eval (DeleteBy _ _ '[]) = '[] +type instance Eval (DeleteBy p x (y ': ys)) = + If (Eval (x `p` y)) ys (y ': Eval (DeleteBy p x ys)) + +data Foldl :: (b -> a -> Exp b) -> b -> t a -> Exp b +type instance Eval (Foldl _ e '[]) = e +type instance Eval (Foldl f e (x ': xs)) = Eval (Foldl f (Eval (f e x)) xs) + diff --git a/src/Units/Simple/Quantity.hs b/src/Units/Simple/Quantity.hs new file mode 100644 --- /dev/null +++ b/src/Units/Simple/Quantity.hs @@ -0,0 +1,80 @@ +{-# OPTIONS_GHC -Wno-missing-methods #-} + +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +module Units.Simple.Quantity + ( Quantity (..) + ) where + +import GHC.TypeLits + +import Units.Simple.Unit + +-- |A numerical quantity with some associated unit. +-- Units are not created directly with this constructor, +-- but through the individual unit functions. +-- +-- Examples: +-- +-- >>> meter -- a unitary quantity associated to meters. +-- 1 m +-- >>> 2.5*ampere -- constructing through literal arithmetic +-- 2.5 A +-- >>> candela' 3.14 -- constructing through the unit constructors +-- 3.14 cd +-- >>> :set -XDataKinds +-- >>> 2 :: Quantity (SingleUnit 'Second) Rational +-- 2 % 1 s +-- +-- Associated units are represented through a phantom parameter of the @Units@ kind synonym. +-- These are currently implemented as a type-level pair of lists representing the power +-- to which each unit is raised. Units can be inspected through @showUnits@. +-- +-- New constructors may be written by combining the provided ones, such as +-- +-- >>> let newton = kilogram .* meter ./ (second .* second) +-- >>> 23*newton +-- 23.0 kg*m/s^2 +-- +-- >>> let g = 6.67408e-11 * newton .* (meter .* meter) ./ (kilogram .* kilogram) +-- >>> g -- gravitational constant +-- 6.67408e-11 m^3/kg*s^2 +-- >>> let gravity m1 m2 r = g .* (m1 * kilogram) .* (m2 * kilogram) ./ (r*meter .* r*meter) +-- >>> let earth_mass = 5.972e24 * kilogram +-- >>> let mars_mass = 6.417e23 * kilogram +-- >>> let earth_radius = 6371e3 * meter +-- >>> let mars_radius = 3389.5e3 * meter +-- >>> let weight_on_earth mass = gravity mass earth_mass earth_radius +-- >>> let weight_on_mars mass = gravity mass mars_mass mars_radius +-- >>> weight_on_earth (80 * kilogram) +-- 785.5719790179963 kg*m/s^2 +-- >>> weight_on_mars (80 * kilogram) +-- 298.22370259533704 kg*m/s^2 +-- >>> fromQuantity $ weight_on_mars 1 / (fromQuantity $ weight_on_earth 1) +-- 0.3796261966575378 +newtype Quantity (us :: Units) a = + Quantity { + fromQuantity :: a -- ^Unwraps a @Quantity@, losing all unit information + } + deriving ( Eq + , Ord + , Enum + , Num + , Real + , Integral + , Fractional + , Floating + , Functor + ) + +instance (KnownSymbol (UnitRepr us), Show a) => Show (Quantity us a) where + show (Quantity x) = show x <> " " <> showUnits @us + +instance Applicative (Quantity us) where + pure = Quantity + Quantity f <*> Quantity x = Quantity (f x) diff --git a/src/Units/Simple/Unit.hs b/src/Units/Simple/Unit.hs new file mode 100644 --- /dev/null +++ b/src/Units/Simple/Unit.hs @@ -0,0 +1,63 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE TypeFamilies #-} +module Units.Simple.Unit where + +import Data.Proxy +import GHC.TypeLits hiding (type (<=)) + +import Fcf hiding (type (<=)) + +import Units.Simple.Internals (Show', Intersperse, Sort, type (<=)) + +data Unit = Meter + | Kilogram + | Second + | Ampere + | Kelvin + | Mole + | Candela + deriving (Eq, Ord, Show) + +type Unit' = (Unit, Nat) +type Units = ([Unit'], [Unit']) + +type family UnitSymbol (u :: Unit) :: Symbol +type instance UnitSymbol 'Meter = "m" +type instance UnitSymbol 'Second = "s" +type instance UnitSymbol 'Kilogram = "kg" +type instance UnitSymbol 'Ampere = "A" +type instance UnitSymbol 'Kelvin = "K" +type instance UnitSymbol 'Mole = "mol" +type instance UnitSymbol 'Candela = "cd" + +data ShowUnit :: Unit' -> Exp Symbol +type instance Eval (ShowUnit '(u, n)) = + If (Eval (TyEq n 1)) + (UnitSymbol u) + (UnitSymbol u `AppendSymbol` "^" `AppendSymbol` Eval (Show' n)) + +type ShowUnitList (ul :: [Unit']) = Eval (Intersperse "*" =<< Map ShowUnit =<< Sort ul) + +type UnitRepr' (num :: [Unit']) (denom :: [Unit']) = + If (Eval (Eval (Null num) && Eval (Null denom))) + "" + (If (Eval (Null denom)) + (ShowUnitList num) + (If (Eval (Null num)) + ("1/" `AppendSymbol` ShowUnitList denom) + (ShowUnitList num `AppendSymbol` "/" `AppendSymbol` ShowUnitList denom))) + +type UnitRepr (us :: Units) = UnitRepr' (Eval (Fst us)) (Eval (Snd us)) + +-- | A string representation of "Units". Useful for debugging. +showUnits :: forall us. KnownSymbol (UnitRepr us) => String +showUnits = symbolVal (Proxy @(UnitRepr us)) + +type instance Eval ((a :: Unit) <= (b :: Unit)) = Eval (UnitSymbol a <= UnitSymbol b)