CS代写 Functional Programming Languages

Functional Programming Languages

The Functional Paradigm MinHS

Copyright By PowCoder代写 加微信 powcoder

Functional Programming Languages

̊man Pohjola

Term 3 2021

The Functional Paradigm MinHS

Functional Programming
Many languages have been called functional over the years:

(define (max-of lst)

[(= (length lst) 1) (first lst)]
[else (max (first lst) (max-of (rest lst)))]))

maxOf :: [Int] → Int
maxOf = foldr1 max

JavaScript?
function maxOf(arr) {

var max = arr .reduce(function(a, b) {
return Math.max(a, b);

What do they
have in common?

The Functional Paradigm MinHS

Definitions

Unlike imperative languages, functional programming languages
are not very crisply defined.

Attempt at a Definition

A functional programming language is a programming language
derived from or inspired by the λ-calculus, or derived from or
inspired by another functional programming language.

The result? If it has λ in it, you can call it functional.

In this course, we’ll consider purely functional languages, which
have a much better definition.

The Functional Paradigm MinHS

Why Study FP Languages?

Think of a major innovation in the area of programming languages.

Garbage Collection?

Lisp, 1958

Functions as Values?
Lisp, 1958

Polymorphism?

Type Inference?

Metaprogramming?

Lisp, 1958

Lazy Evaluation?

Miranda, 1985

Haskell, 1991

Software Transactional Memory?

GHC Haskell, 2005

The Functional Paradigm MinHS

Purely Functional Programming Languages
The term purely functional has a very crisp definition.

Definition

A programming language is purely functional if β-reduction (or
evaluation in general) is actually a confluence.
In other words, functions have to be mathematical functions, and
free of side effects.

Consider what would happen if we allowed effects in a functional

count = 0;
f x = {count := count + x ; return count};
m = (λy . y + y) (f 3)

If we evaluate f 3 first, we will get m = 6, but if we β-reduce m
first, we will get m = 9. ⇒ not confluent.

The Functional Paradigm MinHS

Making a Functional Language

We’re going to make a language called MinHS.

1 Three types of values: integers, booleans, and functions.

2 Static type checking (not inference)

3 Purely functional (no effects)

4 Call-by-value (strict evaluation)

In your Assignment 1, you will be implementing an evaluator for a
slightly less minimal dialect of MinHS.

The Functional Paradigm MinHS

Integers n ::= · · ·
Identifiers f , x ::= · · ·
Literals b ::= True | False
Types τ ::= Bool | Int | τ1 → τ2
Infix Operators ~ ::= * | + | == | · · ·
Expressions e ::= x | n | b | (e) | e1 ~ e2

| if e1 then e2 else e3
| recfun f :: (τ1 → τ2) x = e
↑ Like λ, but with recursion.

As usual, this is ambiguous concrete syntax. But all the
precedence and associativity rules apply as in Haskell. We assume
a suitable parser.

The Functional Paradigm MinHS

Example (Stupid division by 5)

recfun divBy5 :: (Int→ Int) x =

else 1 + divBy5 (x − 5)

Example (Average Function)

recfun average :: (Int→ (Int→ Int)) x =
recfun avX :: (Int→ Int) y =

(x + y) / 2

As in Haskell, (average 15 5) = ((average 15) 5).

The Functional Paradigm MinHS

We don’t need no let

This language is so minimal, it doesn’t even need let expressions.
How can we do without them?

let x :: τ1 = e1 in e2 :: τ2 ≡ (recfun f :: (τ1 → τ2) x = e2) e1

The Functional Paradigm MinHS

Abstract Syntax

Moving to first order abstract syntax, we get:

Concrete Syntax Abstract Syntax

if c then t else e (If c t e)
e1 e2 (Apply e1 e2)
recfun f :: (τ1 → τ2) x = e (Recfun τ1 τ2 f x e)

What changes when we move to higher order abstract syntax?

1 Var terms go away – we use the meta-language’s variables.

2 (Recfun τ1 τ2 f x e) now uses meta-language abstraction:
(Recfun τ1 τ2 (f . x . e)).

The Functional Paradigm MinHS

Working Statically with HOAS

We’re going to write code for an AST and pretty-printer for MinHS
with HOAS.
Seeing as this requires us to look under abstractions without
evaluating the term, we have to extend the AST with special “tag”

The Functional Paradigm MinHS

Static Semantics
To check if a MinHS program is well-formed, we need to check:

1 Scoping – all variables used must be well defined
2 Typing – all operations must be used on compatible types.

Our judgement is an extension of the scoping rules to include types:

Under this context of assumptions

The expression is assigned this type

The context Γ includes typing assumptions for the variables:

x : Int, y : Int ` (Plus x y) : Int

The Functional Paradigm MinHS

Static Semantics

Γ ` (Num n) : Int Γ ` (Lit b) : Bool
Γ ` e1 : Int Γ ` e2 : Int

Γ ` (Plus e1 e2) : Int
Γ ` e1 : Bool Γ ` e2 : τ Γ ` e3 : τ

Γ ` (If e1 e2 e3) : τ

(x : τ) ∈ Γ
Γ ` (Var x) : τ

Γ, x : τ1, f : (τ1 → τ2) ` e : τ2
Γ ` (Recfun τ1 τ2 (f . x . e)) : τ1 → τ2

Γ ` e1 : τ1 → τ2 Γ ` e2 : τ1
Γ ` (Apply e1 e2) : τ2

Let’s implement a type checker.

The Functional Paradigm MinHS

Dynamic Semantics

Structural Operational Semantics (Small-Step)

Initial states: All well typed expressions.
Final states: (Num n), (Lit b), Recfun too!

Evaluation of built-in operations:

e1 7→ e ′1
(Plus e1 e2) 7→ (Plus e ′1 e2)

(and so on as per arithmetic expressions)

The Functional Paradigm MinHS

Specifying If

e1 7→ e ′1
(If e1 e2 e3) 7→ (If e ′1 e2 e3)

(If (Lit True) e2 e3) 7→ e2

(If (Lit False) e2 e3) 7→ e3

The Functional Paradigm MinHS

How about Functions?
Recall that Recfun is a final state – we don’t need to evaluate it
unless it’s applied to an argument.

Evaluating function application requires us to:

1 Evaluate the left expression to get a Recfun;

2 evaluate the right expression to get an argument value; and

3 evaluate the function’s body, after supplying substitutions for
the abstracted variables.

(Apply e1 e2) 7→ (Apply e′1 e2)

(Apply (Recfun . . . ) e2) 7→ (Apply (Recfun . . . ) e′2)

(Apply (Recfun τ1 τ2 (f .x . e)) v) 7→ e[x := v , f := (Recfun τ1 τ2 (f .x . e))]

The Functional Paradigm

程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com