{-# LANGUAGE
DataKinds
, FlexibleContexts
, GADTs
, LambdaCase
, MultiParamTypeClasses
, OverloadedStrings
, PolyKinds
, QuantifiedConstraints
, RankNTypes
, ScopedTypeVariables
, TypeApplications
, TypeFamilies
, TypeOperators
, UndecidableInstances
#-}
module Squeal.PostgreSQL.Type.List
(
SOP.NP (..)
, (*:)
, one
, Join
, disjoin
, Additional (..)
, Path (..)
, Elem
, In
, Length
) where
import Control.Category.Free
import Data.Function ((&))
import Data.Kind
import Data.Type.Bool
import GHC.TypeLits
import Generics.SOP as SOP
type family Join xs ys where
Join '[] ys = ys
Join (x ': xs) ys = x ': Join xs ys
disjoin
:: forall xs ys expr. SListI xs
=> NP expr (Join xs ys)
-> (NP expr xs, NP expr ys)
disjoin = case sList @xs of
SNil -> \ys -> (Nil, ys)
SCons -> \(x :* xsys) ->
case disjoin xsys of (xs,ys) -> (x :* xs, ys)
class Additional expr where
also :: expr ys -> expr xs -> expr (Join xs ys)
instance Additional (NP expr) where
also ys = \case
Nil -> ys
x :* xs -> x :* (xs & also ys)
(*:) :: f x -> f y -> NP f '[x,y]
x *: y = x :* y :* Nil
infixl 8 *:
one :: f x -> NP f '[x]
one f = f :* Nil
type family Elem x xs where
Elem x '[] = 'False
Elem x (x ': _) = 'True
Elem x (_ ': xs) = Elem x xs
type family In x xs :: Constraint where
In x xs = If (Elem x xs) (() :: Constraint)
(TypeError ('ShowType x ':<>: 'Text " is not in " ':<>: 'ShowType xs))
type family Length (xs :: [k]) :: Nat where
Length '[] = 0
Length (_ : xs) = 1 + Length xs