CODEWITHSUNDEEP
haskell
kili
kili

Reputation: 33

haskell compile program nothing show

module Arith where

data Term = 
    TmTrue
  | TmFalse
  | If Term Term Term
  | Zero
  | Succ Term
  | Pred Term
  | IsZero Term
  deriving (Show,Eq)

isnumericval :: Term -> Bool
isnumericval Zero    = True
isnumericval (Succ t1) = isnumericval t1
isnumericval t = False

isval TmTrue  = True
isval TmFalse = True
isval t = isnumericval t

eval1 (If TmTrue  t2 t3) = t2
eval1 (If TmFalse t2 t3) = t3
eval1 (If t1 t2 t3) = 
      let t1' = eval1 t1 
      in If t1' t2  t3 
eval1 (Succ t1) =
      let t1' = eval1 t1 
      in Succ t1' 
eval1 (Pred Zero) = Zero
eval1 (Pred (Succ nv1)) | isnumericval nv1 = nv1
eval1 (Pred t1) =
      let t1' = eval1 t1 
      in Pred t1' 
eval1 (IsZero Zero) = TmTrue
eval1 (IsZero (Succ nv1)) | isnumericval nv1 = TmFalse 
eval1 (IsZero t1) = 
      let t1' = eval1 t1 
      in IsZero t1' 
eval1 t = t -- otherwise, no need to evaluate

eval t =
  let t' = eval1 t
  in if t' == t then t else eval t 


tes1 = print( eval (Succ (Pred Zero)))

i would like to ask about this code, how can i compile this program in haskell? i try to load module such with ghci but nothing show. i want to call and evaluate tes1 , but how can i call it?

Upvotes: 0

Views: 80

Answers (1)

leftaroundabout
leftaroundabout

Reputation: 120751

Here's a step-by-step guide how to deal with such a situation.

  1. Creating file Arith.hs, with the code you gave

  2. $ ghci Arith.hs on the shell.

    [1 of 1] Compiling Arith            ( Arith.hs, interpreted )
Ok, one module loaded.
*Arith>

  3. *Arith> tes1

  4. Nothing seems to happen here, the prompt is frozen. This happens somewhat often in Haskell, since the recursion style can easily be done to get an infinite loop (and unlike in Agda or Coq, there's no totality checker). You can get out of this by hitting ctrl+c:

    *Arith> tes1
^CInterrupted.

  5. So where's the problem? There are a couple of ways to find this out. In this case, I would just toy around in GHCi a bit, in particular see if already eval1 has the same behaviour:

    *Arith> eval1 $ Succ (Pred Zero)
Succ Zero

    Ok, so that seems to be ok. Also if I call it multiple times (as eval might do in proper operation)?

    *Arith> take 6 . iterate eval1 $ Succ (Pred Zero)
[Succ (Pred Zero),Succ Zero,Succ Zero,Succ Zero,Succ Zero,Succ Zero]

    Looks pretty good and indeed converges against the fixpoint that eval is supposed to find.

  6. So that means the problem is in eval. Fortunately that is a really small function, so just go through its evaluation manually in your head.

    eval $ Succ (Pred Zero)
 ≡ let t' = eval1 $ Succ (Pred Zero)
          ≡ Succ Zero
   in if t' == Succ (Pred Zero)
       then Succ (Pred Zero)
       else eval $ Succ (Pred Zero)

    Ok, the t' == Succ (Pred Zero) condition is not fulfilled, so we go into the else branch, where... oops, we've seen eval $ Succ (Pred Zero) before, right? It's what we started with! So that bit is wrong. What you actually want is recurse on the reduced form, i.e. 

    eval t =
   let t' = eval1 t
   in if t' == t then t else eval t'

Upvotes: 3

Related Questions