Sergei Winitzki winitzki

Advanced Functional Programming with Scala - Notes

1. Mastering Functions

A function is a mapping from one set, called a domain, to another set, called the codomain. A function associates every element in the domain with exactly one element in the codomain. In Scala, both domain and codomain are types.

val square : Int => Int = x => x * x

	import scala.compiletime.ops.boolean.&&

	type Sudoku[A <: Tuple] = A match {
	case (
	_1_1 : _1_2 : _1_3 : _1_4 : _1_5 : _1_6 : _1_7 : _1_8 : _1_9 *:
	_2_1 : _2_2 : _2_3 : _2_4 : _2_5 : _2_6 : _2_7 : _2_8 : _2_9 *:
	_3_1 : _3_2 : _3_3 : _3_4 : _3_5 : _3_6 : _3_7 : _3_8 : _3_9 *:
	_4_1 : _4_2 : _4_3 : _4_4 : _4_5 : _4_6 : _4_7 : _4_8 : _4_9 *:
	_5_1 : _5_2 : _5_3 : _5_4 : _5_5 : _5_6 : _5_7 : _5_8 : _5_9 *:
	_6_1 : _6_2 : _6_3 : _6_4 : _6_5 : _6_6 : _6_7 : _6_8 : _6_9 *:

	{-# OPTIONS --without-K #-}
	module C where

	open import Function
	open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; trans; cong; sym)
	open import Data.Empty
	open import Data.Bool
	open import Data.Product as Prod using (∃-syntax; Σ-syntax; _,_; _×_; ∃; proj₁; proj₂)
	open import Data.Maybe as Maybe using (Maybe; just; nothing; is-just)
	open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)

	### Keybase proof

	I hereby claim:

	* I am winitzki on github.
	* I am winitzki (https://keybase.io/winitzki) on keybase.
	* I have a public key ASCGlyC2foE8dsomD34cEbdGXNtkOVwUbyRSnQ3vwSV_Igo

	To claim this, I am signing this object: