1

I'm currently writing a function for substitution (Lambda Calculus) based in Haskell.

data Term = Var String 
          | Application Term Term
          | Lambda String Term

The function takes in a Term t1, String s and a Term t2. The function should replace every occurrence of s in t1 with t2.

subst :: Term -> String -> Term -> Term
subst (Lambda y e) x v = if x == y then (Lambda y e) else let e' = (subst e x v) in (Lambda y e')
subst (Var y) x v = if x == y then v else (Var y)
subst (Application e1 e2) x v = Application (subst e1 x v) (subst e2 x v)

When I try to call the function, I receive the following:

Input

 subst (Lambda "x" (Application (Var "x") (Var "y"))) "y" (Var "f")

Output

subst (Lambda "x" (Application (Var "x") (Var "y"))) "y" (Var "f")
  :: Term

Am I making an input error or is there a problem with my function?

2
  • 2
    How are you trying to call the function? Commented Jan 6, 2022 at 17:51
  • 2
    I could not reproduce this. Are you sure you didn't actually put :t in front, as in :t subst (Lambda ...)? Commented Jan 6, 2022 at 19:54

1 Answer 1

1

The problem is that your Term type lacks a Show instance, and cannot be shown. The interpreter is telling you that the expression foo yielded a result of type SomeType, but it can't print any more details than that because SomeType does not support Show. Your function has therefore apparently returned some value successfully, but you don't know what value. You could inspect it by pattern-matching on the result. But you probably just want to add deriving Show to the type definition, so that the repl can print the value it got.

Now, the most popular repl, GHCI, doesn't normally behave this way: if you try to show a value without a Show instance, you just get an error. But some other GHCI-like tools do this compromise of printing the expression again and its type. One that I know of is interactive-haskell-mode in Emacs; there may well be others.

Sign up to request clarification or add additional context in comments.

6 Comments

This isn't correct for any version of GHC I've ever seen. If it wants to show a thing and can't, it will say "No instance for (Show Term)" or similar, not re-print the term with its type.
Hm, you're right. I'm probably getting it confused with :t myself.
Adding deriving Show seemed to fix the problem for me. I wasn't using :t so I'm unsure why it would return such an output. As I said adding deriving Show worked, thanks for the help
@DavidLukas Yes I'm using GHCi 8.10.7 through Emacs Haskell Mode. By defining the custom definitions for data Term, I call the substitute function as: subst (Lambda "x" (Application (Var "x") (Var "y"))) "y" (Var "f")
@DanielWagner Actually, vikingr12's comment convinced me: I do get this behavior in a GHCI-like thing, but not actually GHCI. Emacs's interactive-haskell mode behaves this way.
|

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.