deontic-core-0.2.0.0: Type-level stratified deontic logic framework
Safe HaskellSafe-Inferred
LanguageGHC2021

Deontic.Core.Adjudicate

Description

Core adjudication engine: stratified defeasible reasoning.

The Adjudicate typeclass resolves legal rules via GHC's instance resolution. The Judgment GADT carries the full reasoning chain as a proof term.

Synopsis

Documentation

class Adjudicate act (layers :: [Type]) where Source #

Core typeclass: stratified adjudication

Methods

adjudicate :: act -> Facts act -> Judgment layers Source #

Instances

Instances details
(TypeError ('Text "\48277\51032 \55136\44208 (lacuna): no applicable rule for " ':<>: 'ShowType act) :: Constraint) => Adjudicate act ('[] :: [Type]) Source #

Non-resolution: empty layer stack is a type error (법의 흠결)

Instance details

Defined in Deontic.Core.Adjudicate

Methods

adjudicate :: act -> Facts act -> Judgment '[] Source #

data Judgment (layers :: [Type]) where Source #

Judgment GADT — carries the full reasoning chain in its type

Constructors

JBase :: Verdict -> ArticleRef -> Text -> Judgment '[l]

Direct rule application (bottom layer — any layer token)

JOverride :: Judgment prev -> Verdict -> ArticleRef -> Text -> Judgment (l ': prev)

This layer overrides the verdict from a lower layer

JDelegate :: Judgment prev -> Judgment (l ': prev)

This layer was available but delegated (did not override)

JCounterfactual :: Judgment prev -> SomeJudgment -> Verdict -> ArticleRef -> Text -> Judgment (l ': prev)

Counterfactual: §150-style "deemed fulfilled/unfulfilled" Carries the hypothetical reasoning chain as a SomeJudgment

verdict :: Judgment layers -> Verdict Source #

Extract the final verdict from any judgment

query :: forall act. Adjudicate act (Resolvable act) => act -> Facts act -> Judgment (Resolvable act) Source #

Top-level query using Resolvable to determine the layer stack

data SomeJudgment where Source #

Existential wrapper — hides the layer type for heterogeneous collections

Constructors

SomeJudgment :: Judgment layers -> SomeJudgment 

someVerdict :: SomeJudgment -> Verdict Source #

Extract verdict from an existentially-wrapped judgment

combineVerdicts :: [SomeJudgment] -> Verdict Source #

Combine independent judgments: fold verdicts with meet