程序代写代做代考 Agda compiler Super advanced functional programming – Or: dependently-typed programming in Agda

Super advanced functional programming – Or: dependently-typed programming in Agda

Super advanced functional programming

Or: dependently-typed programming in Agda

Dr. Dominic Mulligan

Programming, Logic, and Semantics Group,

University of Cambridge

Part III, Advanced Functional Programming, March 2017

1

System Fω

Very expressive type theory:

• Used as a compiler intermediate language (e.g. GHC)
• Can embed almost all useful (co)datatypes within it
• Can express common programming abstractions with
higher-kinds

But:

• The monadic abstraction has associated laws
• Must be checked by hand, on pen-and-paper

2

System Fω

Very expressive type theory:

• Used as a compiler intermediate language (e.g. GHC)
• Can embed almost all useful (co)datatypes within it
• Can express common programming abstractions with
higher-kinds

But:

• The monadic abstraction has associated laws
• Must be checked by hand, on pen-and-paper

2

Internalising reasoning about programs

How can we internalise this checking of laws?

Requires an embedded higher-order logic

Requires types that depend on terms:

∀x : N. x+ 0 = x

is a type, and its inhabitants are proofs

Moved from left plane to right plane of λ-cube

3

Internalising reasoning about programs

How can we internalise this checking of laws?

Requires an embedded higher-order logic

Requires types that depend on terms:

∀x : N. x+ 0 = x

is a type, and its inhabitants are proofs

Moved from left plane to right plane of λ-cube

3

Internalising reasoning about programs

How can we internalise this checking of laws?

Requires an embedded higher-order logic

Requires types that depend on terms:

∀x : N. x+ 0 = x

is a type, and its inhabitants are proofs

Moved from left plane to right plane of λ-cube

3

What’s the advantage?

Agda can be seen as both a programming language and a proof

checker

Agda:

• Allows us to encode very powerful invariants in types that
guarantee program correctness

• Acts as a foundation for mathematics, based not on sets, but
on functions and types

4

What’s the advantage?

Agda can be seen as both a programming language and a proof

checker

Agda:

• Allows us to encode very powerful invariants in types that
guarantee program correctness

• Acts as a foundation for mathematics, based not on sets, but
on functions and types

4

Rest of this lecture: an interactive introduction to Agda…

5