Adding an Ord instance to 'singleton' package generated naturals

Question

I am using very simple type-level naturals generated with the singletons package. I am now trying to add an Ord instance to them.

{-# LANGUAGE MultiParamTypeClasses, TemplateHaskell, KindSignatures, DataKinds, ScopedTypeVariables, GADTs, TypeFamilies, FlexibleInstances, TypeOperators, UndecidableInstances, InstanceSigs #-}

module Functions where

import Data.Singletons
import Data.Singletons.TH
import Data.Singletons.Prelude
import Data.Promotion.Prelude

singletons [d|
             data Nat = Z | S Nat
               deriving Eq

             instance Ord Nat where
               (<=)    Z     _  = True
               (<=) (S _)    Z  = False
               (<=) (S n) (S m) = n <= m
             |]

I have been hitting one error after the other. The latest one is:

src/Functions.hs:10:1:
    Couldn't match kind ‘Nat’ with ‘*’
    When matching types
      n0 :: Nat
      t1 :: *
    Expected type: Sing t1
      Actual type: Sing n0
    Relevant bindings include
      n_a9na :: Sing n0 (bound at src/Functions.hs:10:1)
      lambda :: Sing n0 -> Sing m0 -> Sing (Apply (Apply (:<=$) t00) t10)
        (bound at src/Functions.hs:10:1)
    In the second argument of ‘applySing’, namely ‘n_a9na’
    In the first argument of ‘applySing’, namely
      ‘applySing (singFun2 (Proxy :: Proxy (:<=$)) (%:<=)) n_a9na’

src/Functions.hs:10:1:
    Could not deduce (SOrd 'KProxy) arising from a use of ‘%:<=’
    from the context (t00 ~ 'S n)
      bound by a pattern with constructor
                 SS :: forall (z_a9mg :: Nat) (n_a9mh :: Nat).
                       (z_a9mg ~ 'S n_a9mh) =>
                       Sing n_a9mh -> Sing z_a9mg,
               in an equation for ‘%:<=’
      at src/Functions.hs:(10,1)-(18,15)
    or from (t10 ~ 'S n1)
      bound by a pattern with constructor
                 SS :: forall (z_a9mg :: Nat) (n_a9mh :: Nat).
                       (z_a9mg ~ 'S n_a9mh) =>
                       Sing n_a9mh -> Sing z_a9mg,
               in an equation for ‘%:<=’
      at src/Functions.hs:(10,1)-(18,15)
    or from (t00 ~ Apply SSym0 n0, t10 ~ Apply SSym0 m0)
      bound by the type signature for
                 lambda_a9n9 :: (t00 ~ Apply SSym0 n0, t10 ~ Apply SSym0 m0) =>
                                Sing n0 -> Sing m0 -> Sing (Apply (Apply (:<=$) t00) t10)
      at src/Functions.hs:(10,1)-(18,15)
    In the second argument of ‘singFun2’, namely ‘(%:<=)’
    In the first argument of ‘applySing’, namely
      ‘singFun2 (Proxy :: Proxy (:<=$)) (%:<=)’
    In the first argument of ‘applySing’, namely
      ‘applySing (singFun2 (Proxy :: Proxy (:<=$)) (%:<=)) n_a9na’

Does anyone have an idea what the correct way to do this is?

Answer 1

I'm not sure why this is failing. I am equally puzzled by a similar failure I get when implementing compare instead, and even more puzzled by the failure I get when trying the (seemingly simple)

singletons [d| data Nat = Z | S Nat deriving (Eq,Ord) |]

My guess is that something in Ord is off... However, this works. I'm gonna try to take a look at the guts of singleton later.

singletons [d|
              data Nat = Z | S Nat
                 deriving (Eq)

              instance Ord Nat where
                compare = compare'

              compare' :: Nat -> Nat -> Ordering
              compare' Z Z  = EQ
              compare' (S _) Z = GT
              compare' Z (S _) = LT
              compare' (S n) (S m) = compare' n m
             |] 

By the way, I'm using GHC 8.0 here.

EDIT

After poking around in singletons, I've found the real source of problems (and been blown away with how much type-level hackery is possible). Using -ddump-splices from GHC I was able to get the actual Haskell code generated (for the initial code in your question). The offending parts were

instance PEq (Proxy :: Proxy Nat_a7Vb) where
  type (:==) (a_a8Rs :: Nat_a7Vb) (b_a8Rt :: Nat_a7Vb) = Equals_1627424016_a8Rr a_a8Rs b_a8Rt

and

instance POrd (Proxy :: Proxy Nat_a7Vb) where
  type (:<=) (a_aa9e :: Nat_a7Vb) (a_aa9f :: Nat_a7Vb) = Apply (Apply TFHelper_1627428966Sym0 a_aa9e) a_aa9f

Compiling the code generated, I received the slightly more useful error message for both of these

Expecting one more argument to ‘Proxy’
Expected kind ‘Proxy Nat_a7Vb’, but ‘Proxy’ has kind ‘k0 -> *’

pertaining to the (Proxy :: Proxy Nat_a7Vb) in the PEq and POrd classes. That won't compile without -XPolyKinds. Checked the repo for singletons and indeed it tells you that you need -XTypeInType enabled, which in turn enables -XPolyKinds.

So, there is no bug, you just need to add either PolyKinds or TypeInType (I recommend the latter, since that is what the package recommends...) to your LANGUAGE pragmas to get everything to work.

Answer 2

Working with lifted Boolean relations is never comfortable. Booleans erase the very information you're interested in learning, leaving you in the lurch when you want to do anything with the result of your test. Just say no, kids.

There's a better way. "n is less-than-or-equal to m" is a proposition which can be proved with information-rich evidence. One way of proving that one number is less than another is by giving (a singleton representation of) their difference:

data LE n m where
    LE :: Natty z -> LE n (n :+ z)

We can come up with a procedure for testing whether a given number is less than another. le attempts to subtract n from m, and either fails and returns Nothing or produces their difference, as a Natty, and a proof that the subtraction is correct, packed up in the LE constructor.

le :: Natty n -> Natty m -> Maybe (LE n m)
le Zy m = Just (LE m)
le (Sy n) (Sy m) = fmap (\(LE z) -> LE z) (le n m)
le _ _ = Nothing

This idea can be generalised to give us a "strongly-typed compare". When comparing two numbers, you'll either learn that they're equal, or that one is less than the other. (Either (LE n m) (LE m n) also does the job, but this version is slightly more precise.)

data Compare n m where
    LT :: Natty z -> Compare n (n :+ S z)
    EQ :: Compare n n
    GT :: Natty z -> Compare (m :+ S z) m

compare :: Natty n -> Natty m -> Compare n m
compare Zy Zy = EQ
compare Zy (Sy m) = LT m
compare (Sy n) Zy = GT n
compare (Sy n) (Sy m) = case compare n m of
    LT z -> LT z
    EQ -> EQ
    GT z -> GT z

(I lifted this from Hasochism.)

Note that, unlike le, compare is total. It'll always give you a result: every number is either less than, equal to, or greater than every other number. Our goal was to write a procedure to test which of two numbers was smaller, but we also found ourselves proving that numbers are totally ordered, and writing a type-safe subtraction routine, all in the same function.

Another way of looking at compare is as a view over pairs of natural numbers. When you compare two numbers, you learn which one was less and by how much, refining your knowledge of the numbers themselves. Agda's dot-patterns have good support for this notion of refinement:

compare : (n m : Nat) -> Compare n m
compare zero zero = eq
compare zero (suc m) = lt m
compare (suc n) zero = gt n
compare (suc n)            (suc m)           with compare n m
                        -- see how matching on `lt` refines `m` to `n + suc z`
compare (suc n)            (suc .(n + suc z)) | lt z = lt z
compare (suc m)            (suc .m)           | eq = eq
     -- likewise matching on `gt` refines `n` to `m + suc z`
compare (suc .(m + suc z)) (suc m)            | gt z = gt z

---

Anyway, I can't speak to the source of your singletons bug directly, but one reason Ord is kinda difficult to work with for singleton values is that it assumes you're comparing values of the same type:

class Ord a where
    compare :: a -> a -> Ordering

When you're comparing two singletons, they generally won't have the same type! That's the whole point of singletons: their type reflects their value directly. If you have two Natty n values (whose ns match) there's not much point in comparing them, since you already know they're equal; and if they're not equal you can't compare them!

It's eminently reasonable that classes like Ord, which were designed in the simply-typed world, won't necessarily be all that useful in dependently-typed programs. If you're using dependent types, the right way to do it is not to abuse the old tools. Usher in this new world of safe, information-rich programming with open arms!