haskelldenotational-semantics

How to add function and procedure abstractions denotational semantics using haskell?


I want write a haskell program to implement a simple imperative language based on its denotational semantics. I use GHCi, version 8.4.2 on windows. I encountered some issue when implementing function and procedure abstraction described below.

let me describe it. I call it IMP. First, I define abstract syntax. IMP only accept integer. and identifier will be string.

    type      Numeral  = Int      
    type      Ident    = String

    data Command =
                  Skip
                | Assign   (Ident,       Expression)
                | Letin    (Declaration, Command   )
                | Cmdcmd   (Command,     Command   )
                | Ifthen   (Expression,  Command, Command)
                | Whiledo  (Expression,  Command   )
                | IdentifierC ( ActualParameter )

    data Expression =
                Num    Numeral
                | False_
                | True_
                | Notexp   Expression
                | Id       Ident
                | Sumof   (Expression,  Expression)
                | Subof   (Expression,  Expression)
                | Prodof  (Expression,  Expression)
                | Less    (Expression,  Expression)
                | Leten   (Declaration, Expression)
                | IdentifierE ( ActualParameter )
                  deriving Show

    type ActualParameter = Expression

    data FormalParameter = Constfp Identifier

    data Declaration =
              Constdef (Ident,  Expression)
            | Vardef   (Ident,  TypeDef   )
            | Func Identifier ( FormalParameter ) ~ Expression
            | Proce Identifier ( FormalParameter ) ~ Command
              deriving Show

    data TypeDef =
              Bool | Int
              deriving Show

brief explanation: in Command, Skip will do nothing. Assign will give value of the Expression to the Ident. Letin will declare some variable in command. Cmdcmd will run 2 commands sequentially. Ifthen is conditional command, if first expression is evaluated to true, then run first command, second command otherwise. Whiledo is loop. IdentifierC ( ActualParameter ): IdentifierC denotes some function in the local environment. this ActualParameter is some expression with some value. this command jus call this function on the specified value.

in Expression, from top to down are: numeral bool false bool true negate of expression get value of the Ident from the local environment. sum 2 expressions substract 2 expressions product of 2 < declare some variable in expression IdentifierE ( ActualParameter ) IdentifierE denotes some function in the local environment. this ActualParameter is some expression with some value. this command jus call this function on the specified value. finally got a new value as the result of this expression.

then is Semantic Domains

    type    Integer = Int
    type    Boolean = Bool
    type    Location  = Int
    type    Function = Argument -> Store -> Value
    type    Procedure = Argument -> Store -> Store
    -- store would be snapshot of the memory.

    data    Value   = IntValue    Int
                    | TruthValue  Bool
                      deriving (Eq, Show)
    -- first class value only are int and bool

    type    Storable  = Value

    data    Bindable  = Const Value 
                      | Variable Location 
                      | Function Func 
                      | Procedure Proce
                      deriving (Eq, Show)

    data    Denotable = Unbound | Bound Bindable
                      deriving (Eq, Show)

    type    Argument = Value

    data Sval  = Stored Storable | Undef | Unused

    -- The actual storage in a Store
    type DataStore = Location -> Sval

    --                   --bot---   --top---  --data---
    data Store = Store (Location,  Location,  DataStore)

    type  Environ  =  Ident -> Denotable

    -- ---------- Semantic Functions -------------- --
    valuation :: Int         -> Value
    evaluate  :: Expression  -> Environ -> Store ->  Value
    elaborate :: Declaration -> Environ -> Store ->  (Environ,Store)
    execute   :: Command     -> Environ -> Store ->  Store

    -- the main goal is to define these semantic functions
    -- I give some examples in my source code below.

my code is here: https://github.com/sanyuwen/IMP/blob/master/DSemImp.hs. my test code is here: https://github.com/sanyuwen/IMP/blob/master/ImpTest.hs

when I use GHC to import DSemImp module, I encountered many errors.

DSemImp.hs:52:32: error:
    Not in scope: type constructor or class ‘Identifier’
   |
52 | data FormalParameter = Constfp Identifier    |                                ^^^^^^^^^^
It said data FormalParameter = Constfp Identifier is not legal.
without this how can I define formal parameter ??

Solution

  • You didn't define Identifier. Though you defined Ident, is that what you meant?