schema.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Function ((&))
import Data.Kind (Constraint, Type)
import GHC.Generics
import GHC.TypeLits (KnownSymbol, Symbol)

data Optionality = Required | Optional

type SchemaParam = (Symbol, Type, Optionality)

type Schema = [SchemaParam]

type (::!) :: Symbol -> Type -> SchemaParam
type a ::! b = '(a, b, Required)

type (::?) :: Symbol -> Type -> SchemaParam
type a ::? b = '(a, b, Optional)

type Optionals :: [(Symbol, Type)] -> Schema
type family Optionals kvs = r | r -> kvs where
  Optionals '[] = '[]
  Optionals ('(k, v) : kvs) = k ::? v : Optionals kvs

type Params :: Schema -> Type
data Params s where
  ParamsNil :: forall s. Params (Optionals s)
  ParamsSkip :: forall k v {s}. Params s -> Params (k ::? v : s)
  ParamsCons :: forall k v o {s}. v -> Params s -> Params ('(k, v, o) : s)

type UnParam :: SchemaParam -> Type
type family UnParam sp where
  UnParam (k ::! v) = v
  UnParam (k ::? v) = Maybe v

data Nat = Zero | Succ Nat

type Index :: a -> [a] -> Nat
type family Index x xs where
  Index x (x : _) = Zero
  Index x (_ : xs) = Succ (Index x xs)

type HasParam :: SchemaParam -> Schema -> Nat -> Constraint
class HasParam sp s i where
  lookupParam' :: Params s -> UnParam sp

instance HasParam (k ::! v) (k ::! v : s) Zero where
  lookupParam' (ParamsCons x _) = x

instance HasParam (k ::? v) (k ::? v : s) Zero where
  lookupParam' = \case
    ParamsCons x _ -> Just x
    ParamsSkip _ -> Nothing

instance HasParam sp s i => HasParam sp (x : s) (Succ i) where
  lookupParam' = \case
    ParamsCons _ xs -> lookupParam' @sp @s @i xs
    ParamsSkip xs -> lookupParam' @sp @s @i xs

lookupParam :: forall sp s. HasParam sp s (Index sp s) => Params s -> UnParam sp
lookupParam = lookupParam' @sp @s @(Index sp s)

type SchemaResolved :: Type -> Schema -> Constraint
class SchemaResolved a s where
  resolve :: Params s -> a
  default resolve :: (Generic a, GSchemaResolved (Rep a) s) => Params s -> a
  resolve p = to (gresolve @(Rep a) @s p)

type GSchemaFor :: (Type -> Type) -> Schema -> Constraint
type family GSchemaFor rep s where
  GSchemaFor (D1 m cons) s = GSchemaFor cons s
  GSchemaFor (C1 m sels) s = GSchemaFor sels s
  GSchemaFor (s1 :*: s2) s = (GSchemaFor s1 s, GSchemaFor s2 s)
  GSchemaFor (S1 (MetaSel (Just k) _ _ _) (Rec0 (Maybe v))) s = HasParam (k ::? v) s (Index (k ::? v) s)
  GSchemaFor (S1 (MetaSel (Just k) _ _ _) (Rec0 v)) s = HasParam (k ::! v) s (Index (k ::! v) s)

type HasSchema :: Type -> Schema -> Constraint
type HasSchema a s = GSchemaFor (Rep a) s

type GSchemaResolved :: (Type -> Type) -> Schema -> Constraint
class GSchemaResolved rep s where
  gresolve :: Params s -> rep a

instance GSchemaResolved cons s => GSchemaResolved (D1 m cons) s where
  gresolve p = M1 (gresolve p)

instance GSchemaResolved sels s => GSchemaResolved (C1 m sels) s where
  gresolve p = M1 (gresolve p)

instance (GSchemaResolved s1 s, GSchemaResolved s2 s) => GSchemaResolved (s1 :*: s2) s where
  gresolve p = gresolve p :*: gresolve p

instance {-# OVERLAPS #-} HasParam (k ::? v) s (Index (k ::? v) s) => GSchemaResolved (S1 (MetaSel (Just k) m2 m3 m4) (Rec0 (Maybe v))) s where
  gresolve p = M1 (K1 (lookupParam @(k ::? v) p))

instance HasParam (k ::! v) s (Index (k ::! v) s) => GSchemaResolved (S1 (MetaSel (Just k) m2 m3 m4) (Rec0 v)) s where
  gresolve p = M1 (K1 (lookupParam @(k ::! v) p))

data X = X {b :: Maybe String, a :: Int}
  deriving stock (Generic)

deriving anyclass instance HasSchema X s => SchemaResolved X s

schema :: Params ["a" ::! Int, "b" ::? String, "c" ::! Bool, "d" ::? Int]
schema =
  ParamsCons @"a" @Int @Required 42 $
    ParamsSkip @"b" @String $
      ParamsCons @"c" @Bool @Required True $
        ParamsNil

x :: X
x = resolve schema