ラムダ計算をHaskellで書いてる途中。自由変数がいくつあるかを型に埋め込みたいと思った。やっぱりGADTにした。

LC.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeSynonymInstances #-}
-- {-# LANGUAGE StandaloneDeriving #-}
-- {-# LANGUAGE FlexibleInstances #-}
-- {-# LANGUAGE ImpredicativeTypes #-}

import Control.Monad.Reader hiding (join)

data TermP v where
  TmVar :: v -> TermP v
  TmAbs :: OpenTerm ClosedTerm v -> TermP v
  TmApp :: TermP v -> TermP v -> TermP v

type ClosedTerm = TermP
newtype OpenTerm p v = OpenTerm (v -> Term p v)

data Term p v where
  ClosedTerm :: TermP v -> Term ClosedTerm v
  UseFreeVar :: (v -> Term p v) -> Term (OpenTerm p) v

isValue :: Term p v -> Bool
isValue (UseFreeVar f) = isValue (f undefined)
isValue (ClosedTerm tm) = go tm
  where
    go t = case t of
      TmVar _ -> True
      TmAbs _ -> True
      TmApp (TmAbs _) _ -> False
      TmApp a b -> go a && go b