haskell specifying ordered list in type signature

In haskell I can specify with type signature of function f that pair must be ordered in this way:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}

module Main where 
import Data.Kind

data Nat = Z | S Nat deriving Show
type One = S Z
type Two = S One

data SNat (n :: Nat) where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)
  
  
f :: (Gt a b) => (SNat a, SNat b) -> SNat b
f (a,b) = b

-- comparing two types:
type Gt :: Nat -> Nat -> Constraint
type family Gt n m where
  Gt Z _ = 'True ~ 'False
  Gt _ Z = ()
  Gt (S n) (S m) = Gt n m

Now I can construct only ordered pairs:

:t f (SS SZ, SZ)

Or I can go with hlist:

type HList :: [Type] -> Type
data HList xs where
  HNil :: HList '[]
  (:&) :: x -> HList xs -> HList (x : xs)
infixr 5 :&

And I can do function for 2 elements:

g2 :: (Gt a b) => HList [SNat a, SNat b]
g2 (a :& b :& HNil) = b

for 3:

g3 :: (Gt a b, Gt a c, Gt b c) => HList [SNat a, SNat b, SNat c]
g3 (a :& b :& c :& HNil) = c

Continue to grow into complex type signatures of g4, g5 ..

Is it possible to write general function that specify in type signature "Only list of numbers that ordered" for arbitary length list, so something like:

gn :: "Some magic" => [Snat a]

After this all non ordered list rejected by type system.

Solution

You would really want singletons for lists:

-- "proto-SList"
-- also "proto-HList", since HList ~= SList' Identity
data SList' (f :: a -> Type) (xs :: [a]) :: Type where
    SNil :: SList' f '[]
    SCons :: f x -> SList' f xs -> SList' f (x : xs)
infixr 5 `SCons`
type SListNat = SList' SNat -- a proper "SList" requires having a "Sing" type/data family, that determines the function f from the element type a

Then define sortedness, as a type family [Nat] -> Constraint, in the obvious way

type family Descending (xs :: [Nat]) :: Constraint where
    Descending '[] = ()
    Descending '[_] = ()
    Descending (x : y : xs) = (Gt x y, Descending (y : xs))

Then you may define g.

g :: Descending xs => SListNat xs -> ()
g SNil = ()
-- note how recursive structure *must* follow structure of Descending
g (x `SCons` SNil) = ()
g (x `SCons` y `SCons` xs) = g (y `SCons` xs)

correct :: ()
correct = g (SS (SS SZ) `SCons` SS SZ `SCons` SZ `SCons` SNil)
incorrect :: ()
incorrect = g (SZ `SCons` SS (SS SZ) `SCons` SS SZ `SCons` SZ `SCons` SNil)

If you really must use HList, you could e.g. strip off all the SNats before using Descending (or modify Descending accordingly)

-- using two type families is *necessary*, the equation StripSNats (SNat x : xs) = x : StripSNats xs does *not* work
-- this kind of weirdness is why you should avoid using HList for this purpose
type family StripSNat (x :: Type) :: Nat where StripSNat (SNat x) = x
type family StripSNats (xs :: [Type]) :: [Nat] where
    StripSNats '[] = '[]
    StripSNats (x : xs) = StripSNat x : StripSNats xs
g' :: Descending (StripSNats xs) => HList xs -> ()
g' HNil = ()
g' (x :& HNil) = ()
g' (x :& y :& xs) = g' (y :& xs)