Is "syntactically correct by construction" worth it?

[LightAndLight]

Until now, the approach to the AST has been "as correct-by-construction as possible, falling back to smart constructors when necessary". Since we've been getting closer to a complete representation, I have been considering another approach that gets similar levels of safety but permits a more elegant library design, and potentially better user experience.

Here it is, applied to a very small AST:

{-# language DataKinds, PolyKinds, LambdaCase, ViewPatterns #-}
module AST (AST, Val(..), _Int, _Add, _Assign, unvalidate, validate) where

import Control.Lens
import Data.Coerce

data Val = UV | V

data AST (a :: Val)
  = Int Int
  | Add (AST a) (AST a)
  | Assign String (AST a)
  deriving (Eq, Show)

_Int :: Prism (AST a) (AST UV) Int Int
_Int =
  prism
    Int
    (\case; (unvalidate -> Int a) -> Right a; (unvalidate -> a) -> Left a)

_Add :: Prism (AST a) (AST UV) (AST UV, AST UV) (AST UV, AST UV)
_Add =
  prism
    (uncurry Add)
    (\case; (unvalidate -> Add a b) -> Right (a, b); (unvalidate -> a) -> Left a)

_Assign :: Prism (AST a) (AST UV) (String, AST UV) (String, AST UV)
_Assign =
  prism
    (uncurry Assign)
    (\case; (unvalidate -> Assign a b) -> Right (a, b); (unvalidate -> a) -> Left a)

unvalidate :: AST a -> AST UV
unvalidate = coerce

validate :: AST UV -> Maybe (AST V)
validate (Int a) = Just $ coerce $ Int a
validate (Add a b) =
  fmap coerce $
  Add <$> (coerce <$> validate a) <*> (coerce <$> validate b)
validate (Assign a b)
  | a == "bad" = Nothing
  | otherwise =
    fmap coerce $
    Assign a <$> (coerce <$> validate b)

In this approach, I use a phantom type to indicate that the AST has been validated. Due to the types of the prisms, only unvalidated terms can be constructed, but terms of any validation status can be matched on. This means we can use the same data structure to represent validated and unvalidated terms. The current codebase has two distinct datatypes (with a lot of duplication). The other consequence is that all syntax-correction checking is moved to run-time. I don't believe this is a bad thing, considering the amount of checks that are already performed at run-time.

This pattern also fixes the optics problem that is demonstrated in #17.

There is a small "safety" flaw with this approach, that a user can just use coerce to skip the validation stage. Currently I think that's an okay trade-off.