Guaranteeing at the type level uniqueness of members and length of a list-like data-type for safe specification of finite Linear Orders.

0-FiniteLinearOrder.hs

{-# LANGUAGE GADTs, TypeFamilies, TypeOperators #-}
{-# LANGUAGE ConstraintKinds, DataKinds, PolyKinds #-}

module FiniteLinearOrder (
  FullFiniteLinearOrder (..),
  FiniteLinearOrder (..),
  Nat (..),
) where

import GHC.Exts (Constraint)

-- Private type family checking membership of type-level lists.
type family Elem (x :: k) (xs :: [k]) :: Bool where
  Elem a '[]       = 'False
  Elem a (a ': bs) = 'True
  Elem a (b ': bs) = Elem a bs

-- List-like GADT over a typeclass, tracking the types of its members.
-- Ensures uniqueness of members at construction.
data FullFiniteLinearOrder :: [*] -> (* -> Constraint) -> * where
  Empty :: FullFiniteLinearOrder '[] c
  (:>:) :: (c a, Elem a m ~ 'False)
        => a -> FullFiniteLinearOrder m c -> FullFiniteLinearOrder (a ': m) c

infixr 6 :>:

-- Naturals for promoted use.
data Nat = Z | S Nat
  deriving (Show, Read, Eq, Ord)

-- Private type family calculating the length of type-level lists.
type family Length (xs :: [k]) :: Nat where
  Length '[]       = 'Z
  Length (b ': bs) = 'S (Length bs)

-- A version of @FullFiniteLinearOrder@ that (crucially) obscures the order of
-- its members at the type-level. This would not be necessary if we used
-- type-level sets rather than lists.
data FiniteLinearOrder :: Nat -> (* -> Constraint) -> * where
  FiniteLinearOrder
    :: FullFiniteLinearOrder m c -> FiniteLinearOrder (Length m) c

1-CornerLO.hs

{-# OPTIONS_GHC -Wno-unused-top-binds #-}
{-# LANGUAGE LambdaCase, DataKinds, GADTs #-}

module CornerLO (
  CornerLO, fromCLO,
  TL (..), TR (..), BL (..), BR (..),
  Corner (..), Vertical (..), Horizontal (..)
) where

import FiniteLinearOrder

-- Regular @Corner@ product type.
data Corner     = C Vertical Horizontal deriving (Show, Read, Eq, Ord)
data Vertical   = B | T                 deriving (Show, Read, Eq, Ord)
data Horizontal = L | R                 deriving (Show, Read, Eq, Ord)

-- Singleton corners.
data TL = TL deriving (Show, Read)
data TR = TR deriving (Show, Read)
data BL = BL deriving (Show, Read)
data BR = BR deriving (Show, Read)

-- /Private/ (and hence closed) class over singleton corners.
class    IsCorner c  where toCorner :: c -> Corner
instance IsCorner TL where toCorner    TL = C T L
instance IsCorner TR where toCorner    TR = C T R
instance IsCorner BL where toCorner    BL = C B L
instance IsCorner BR where toCorner    BR = C B R

-- Four element Linear Order over the @IsCorner@ class.
type CornerLO = FiniteLinearOrder ('S ('S ('S ('S 'Z)))) IsCorner

-- Reduce a @CornerLO@ down to something we can easily work with.
fromCLO :: CornerLO -> [Corner]
fromCLO (FiniteLinearOrder full) = fromFull full
  where fromFull :: FullFiniteLinearOrder m IsCorner -> [Corner]
        fromFull = \case Empty      -> []
                         (x :>: xs) -> toCorner x : fromFull xs

-- Test @CornerLO@.
cLO :: CornerLO
cLO = FiniteLinearOrder (TL :>: TR :>: BR :>: BL :>: Empty)