Functional Programming Manual V.1

Expressions / Totality / Datatypes & Structural Induction / Functions Types

7 min readFeb 8, 2020

🕴Hey!

This is a short article on the key ideas we’ve covered in the last few weeks. Ideas are visualized through illustrations. Hope you enjoy and gain more clarity regarding the concepts. We, 150 TAs, are always here for you! 💞

The following topics are covered ↘

Expressions
Totality
Datatypes & Structural Induction
Strong Induction
Functions Types

Expressions

🌲 In the beautiful land of Standard ML, we have …

(You can find this in the lab handout for basics_lab)

And we really care about EXPRESSIONS, and whether if they are well-typed. When they are NWT , the SML/NJ compiler will yell at you. 😡

We do not want the broken whatever on the left, instead, we only want the golden egg 🥚💛. We want everything to TYPE CHECK.

There are three possibilities for all well-typed expressions.

could be valuable (*values are valuable!)
could loop forever
could raise an exception

So, why do we care? When do we need to be REALLY careful about it?

Totality & Proofs

When given a piece of code (or your own code), and asked to prove that certain theorem holds, you encounter situations when you are not sure if you can take the step because of a function input that does not look like our regular inputs that are ALREADY values, e.g. 1 ,2, 3, true, false, [1,2,3], [4,5,6], (true, 1), …

Instead, you would have something like listSum(inord L) , and there is no way you can find out what inord L is, but you know that it must be a WT expression. So, let’s go back to our golden egg a.k.a well-typed expressions.

Here you are, holding a WT expression, and knowing where you need to get to, but unsure of whether if you can take the step.

So, we need something to promise us that inside that egg will be a valuable expression. We NEED the inord L in listSum(inord L) to be a value or valuable because SML is a call-by-value, eager language, which just means that functions evaluate their arguments before doing anything else.

✨ ✨ TOTALITY COMES TO RESCUE✨ ✨

By citing totality of inord , we are promised to have inord L as a value or a valuable expression, which allows us to take the step to go on in our proof.

Don’t we all 💘 Induction?

Strong Induction

When you are proving something that involves recursive calls to different smaller values, you probably need strong induction. By assuming the theorem holds for a RANGE of values, you have more to use in your inductive step.

Structural Induction

The cases you have to prove using structural induction should come natural because your proof should follow the datatype.

(* just some pseudo proof structure *)datatype iceCreamFlavor = chocolate | vanilla | strawberryWTS: P(x) holds for all x : iceCreamFlavor Case 1: Let x be chocolate 
Case 2: Let x b vanilla
Case 3: Let x be strawberry

A more complex example would be,

(* just some pseudo proof structure *)datatype starbucks = CannotFind | starbucks * string * starbucksWTS: P(x) holds for all x : starbucksBase Case: Let x be CannotFindI.S.: Let x be (LS, s, RS), where LS : starbucks, s : string, RS : starbucks. I.H.: Assume P(LS) and P(RS) hold. (WTS P(LS, s, RS) holds)

So why does this work?

Let’s take our ice cream 🍦datatype as an example.

datatype iceCreamFlavor = chocolate | vanilla | strawberry

Saying for some theorem P , P(x) holds for all x : iceCreamFlavor , you can visualize as all chocolate | vanilla | strawberry need to jump through the fire hoop of P to prove that P holds for them.

And that’s the beauty of structural induction. You can just simply look at the datatype, and show that they can jump through the hoop successfully.

So when you are trying to figure what to case on, look at the datatype constructors, and you should know what to do.

Also, A rule of thumb to figure out B.C. versus I.S. would be non-recursive cases are base cases, and recursive cases should be proved with I.H. and I.S..

Function Types

Figuring types for functions can be confusing, and how I like to do it is to see fn as a door that only welcomes a specific kind of guest.

Some Ideas:

all functions written using fun keyword can be rewritten using fn
the number of fn you have = the number of arguments you are taking in
the last type in a function type will be the result type
fn should NEVER be in any of your type annotations

~Let’s do some examples~

val f = fn x : int => fn y : bool => (x, y)

So the first door only opens when you give f a int , and the second door only opens when you give f 1 (or any other int) a bool .

f : int -> bool -> (int * bool)

Let’s get a bit more complex!

val g = fn x : int => fn y : int => fn z : bool => fn m : int list => fn b : bool list => fn k : (bool * int) list => (* what you want to return  *)

If you count the fn, we have 6 fns, and here we have 6 doors, hence we can take in 6 arguments

Let’s go back to our previous example of f

val f = fn x : int => fn y : bool => (x, y)f : int -> bool -> (int * bool)

When we give f the argument 1 : int , f sees that, “Oh, it’s a value of type int , I will let her in.”

Then 1 walks into the first door, and now x is bound to 1 . As 1 walks in, 1 has good manners and makes sure she has closed the door 🚪.

f 1 is f with its first door closed.

So the type of f 1 is bool -> int * bool .

f 1 : bool -> (int * bool)val g = f 1 
(* val g = fn y : bool => (1, y) *)

The same goes for constructors with functions types. Recall the following datatypes from the hw,

datatype professor = Erdmann | Pfenningdatatype job = Student | Professor of professor | TA of string

Here we have the two function type constructors Professor of professor and TA of string . You can see them as normal functions that takes in a value (of whatever type it is after of ) and outputs a value of the datatype which the constructors are defined along with.

Professor : professor -> job
TA : string -> job

And we know, val f : string -> bool is a valid function type, so TA : string -> job is also a well-typed expression with a function type. TA is a completely valid function that’s just waiting for its argument of type string.

Recap On Important Ideas

As we come to an end, I would like to jot down some important things to watch out for.

No fn in ANY type annotations
Cite totality when you are assuming some function input must be valuable
Let the datatype lead your structural induction proof
Expression with a function type without inputs is STILL well-typed. It is simply waiting for its input.
FUNCTIONS ARE VALUES