CODEWITHSUNDEEP
haskellghcgadt
flyingsheep
flyingsheep

Reputation: 69

Non-exhaustive patterns with GADT

I want to write a function to transform regular lambda expression to DeBrujin style with data struct defined by GADT style.

{-# 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)

function tranform gets LambdaTerm to LambdaIndex, But on calling transform [] t1 the interpreter gives

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

I'm confused, LambdaTerm has only three constructors.

Upvotes: 1

Views: 136

Answers (1)

chi
chi

Reputation: 116139

I obtained

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

after a small fix

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)

The issues were

  1. a typo, as already pointed out in the comments above;
  2. a redundant type annotation, which can not be used with GADT (apparently).

To identify the issues, I simply loaded the file with warnings enabled (-Wall), and saw the messages:

    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
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

and

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

pointing out the missing case in transform, and an independent transfrom without a signature.

I'd recommend you also turn all warnings on and check out all the other messages. None of them points towards a serious issue, but it's a good habit to clean up the code so that it raises no warnings anyway.

Upvotes: 8

Related Questions