GADT 的非穷举模式

Question

我想编写一个函数，用 GADT 样式定义的数据结构将正则 lambda 表达式转换为 DeBrujin 样式。

{-# Language GADTs, StandaloneDeriving,ScopedTypeVariables #-}

module DeBrujin where

import Debug.Trace
import Data.List as L

data Apply
data Abstract
data Variable

data LambdaTerm a where
  Var :: String -> LambdaTerm Variable
  Abs :: String -> LambdaTerm a -> LambdaTerm Abstract
  App :: LambdaTerm Abstract -> LambdaTerm a -> LambdaTerm Apply

instance Show (LambdaTerm a) where
  show (Var v) = v
  show (Abs s t) = "?" ++ s ++ "." ++ show t
  show (App t1 t2) = "(" ++ show t1 ++ ")" ++ "(" ++ show t2 ++ ")"

t1 = App (Abs "x" (Var "x")) (Var "y")
t2 = Abs "x" (Abs "y" (Var "x"))

data LambdaIndex a where
  VarI :: String -> LambdaIndex Variable
  AbsI :: String -> LambdaIndex a -> LambdaIndex Abstract
  AppI :: LambdaIndex Abstract -> LambdaIndex a -> LambdaIndex Apply
  BoundI :: Int -> LambdaIndex Variable

instance Show (LambdaIndex a) where
  show (VarI v) = v
  show (AbsI s t) = "?." ++ show t
  show (AppI t1 t2) = "(" ++ show t1 ++ ")" ++ "(" ++ show t2 ++ ")"
  show (BoundI i) = show i

t1' = AppI (AbsI "x" (BoundI 0)) (VarI "y")

type Env = [String]

transform :: Env -> LambdaTerm a -> LambdaIndex a
transform e (Var v) = case L.findIndex (v==) e of
                        Just i -> BoundI i
                        Nothing -> VarI v
                        
transform e (Abs s t) = AbsI s (transform (s:e) t)
transfrom e ((App t1 t2)::LambdaTerm Apply) = AppI trans1 trans2
  where
    trans1 = (transform e t1)
    trans2 = (transform e t2)

函数转换将 LambdaTerm 转换为 LambdaIndex，但在调用transform [] t1解释器时给出

*** Exception: DeBrujin.hs:(43,1)-(47,50): 
    Non-exhaustive patterns in function transform

我很困惑，LambdaTerm只有三个构造函数。

Answer 1

我获得了

*DeBrujin> transform [] t1
(?.0)(y)

经过小修

transform :: Env -> LambdaTerm a -> LambdaIndex a
transform e (Var v) = case L.findIndex (v==) e of
                        Just i -> BoundI i
                        Nothing -> VarI v
                        
transform e (Abs s t) = AbsI s (transform (s:e) t)
transform e (App t1 t2) = AppI trans1 trans2
  where
    trans1 = (transform e t1)
    trans2 = (transform e t2)

问题是

1. 正如上面的评论中已经指出的那样，打字错误；
2. 冗余类型注释，不能与 GADT 一起使用（显然）。

为了确定问题，我只是加载了启用警告 ( -Wall)的文件，并看到了消息：

    Pattern match(es) are non-exhaustive
    In an equation for `transform':
        Patterns not matched:
            [] (App _ _)
            (_:_) (App _ _)
   |
42 | transform e (Var v) = case L.findIndex (v==) e of
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

和

    Top-level binding with no type signature:
      transfrom :: [String] -> LambdaTerm Apply -> LambdaIndex Apply
   |
47 | transfrom e ((App t1 t2)::LambdaTerm Apply) = AppI trans1 trans2

指出 中缺少的情况transform，以及transfrom没有签名的独立。

我建议您也打开所有警告并查看所有其他消息。他们都没有指出一个严重的问题，但清理代码是一个好习惯，这样它无论如何都不会引发警告。