Sample Terms for Practical Type Inference for Arbitrary Rank Types

I’ve been heads down over the past few months. I decided to develop sample terms for the paper Practical Type Inference for Arbitrary Rank Types, so I can build some intuition on this topic.

I describe the terms below, but before I do so I’ll briefly explain my motivation. My motivation follows from my past work on Model Driven Architecture, Ontology and Logic(s). The questions that arise naturally in the course of studying these topics lead me to closely examine quantification and type systems. Higher rank types provide both a mechanism for polymorphism and high assurance in the subjects that motivated my study.

I won’t say much about the paper, other than there was no shortage of fun to be had. Many thanks to Dimitrios Vytiniotis for answering my questions. The remaining errors are mine. I recommend working through the paper and developing your own terms. The sections below should provide just enough background to show how my approach evolved over the last few months. There are two parts to the work below. Part 1 – Lambda Terms and Types and Part 2 – Haskell Terms and Types. Both are parsed by the Tc Monad.

Part 1 – Lambda Terms and Types Parsed by Tc Monad.

The sections below illustrate progressive term construction. Section 1 lists very simple terms both explicitly and implicitly typed. Section 2 lists terms of interest up to rank 2 as described in Kfoury [2]. Section 3 lists terms of interest that further illustrate how the Tc Monad evaluates terms subject to alpha, beta and eta reduction. lets, subsumption. Section 4 lists Unification errors and a few surprising successes. Section 5 lists the explicitly quantified principal types derived from terms without explicit quantifiers, then it shows explicitly quantified principal types derived from application and beta reduction of terms. Section 6 lists some changes to the principle types when explicitly annotating terms.

– Except where otherwise noted, I use the following convention to show the input term and the output of the Tc monad. Comments appear to the right of terms.

– input term — output type

– Just uncomment the terms to the left, then validate the result on the right. Comments explain the sepcifics of an example.

-- Section 1 - Implicitly and Explicitly Typed Terms and Types

-- Example 1 - Literal
-- 0 -- 0 :: (forall. Int)

-- Example 2 - Implicitly Typed Term
-- \x. x -- (\x. x) :: (forall a. a -> a) - I combinator

-- Example 3 - Type Constant (Rho Type?) in Typed Abstraction
-- \(x::a). x -- (\(x::a). x) :: (forall. a -> a) -- Confirm the a denotes a type constant, or rho type?

-- Example 4 - Another Type Constant in Typed Abstraction
-- \(x::a). 0 -- (\(x::a). 0) :: (forall. a -> Int)

-- Example 5 - Yet Another
-- \(x::a). \(y::b). y -- (\(x::a). \(y::b). y) :: (forall. a -> b -> b)

-- Example 6 - And Another
-- \(x::Bool). \(y::Bool). y -- (\(x::Bool). \(y::Bool). y) :: (forall. Bool -> Bool -> Bool)

-- Example 7 - Equivalence of Typed Abstraction and Typed Annotation
-- \(x::Int). x -- (\(x::Int). x) :: (forall. Int -> Int) -- typed abstraction
-- \x. x :: Int -- (\x. x :: Int) :: (forall. Int -> Int) -- typed annotation

-- Example 8 - Typed Abstraction Annotated with (Rho Type ?)
-- \(x::(forall. a -> a)). x -- (\(x::(forall. a -> a)). x) :: (forall. (forall. a -> a) -> a -> a) -- Although the universal quantifiers seem to be nested, there's still no type variable to range over the types, so this is still rank 0.

-- Section 2

-- Examples 1 and 3 - 8 are all rank 0 types. Rank 0 types are monotypes. Note that in each rank 0 type the universal quantifier is not followed by a type variable before the dot (forall.). Examples 9 - 10 are rank 1 types. Rank 1 terms are polytypes. Rank 1 types have one or more type variables left of the dot (forall a b.). Examples 11 - x are rank 2 types. Rank 2 terms annotate

-- Example 9 - Type Variable Rank 1
-- \x. \y. x -- (\x. \y. x) :: (forall a b. b -> a -> b) -- K combinator

-- Example 10 - Another Rank 1
-- \x. \y. \z. x z (y z) -- (\x. \y. \z. x z (y z)) :: (forall a b c. (b -> a -> c) -> (b -> a) -> b -> c) -- S combinator

-- Example 11 - Universal Quantifier Annotation on Typed Abstraction, Rank 2
-- \(x::(forall a. a)). 0 -- (\(x::(forall a. a)). 0) :: (forall. (forall a. a) -> Int) -- note there's no quantifier to range over the monotype Int (Is what Andreas said correct ?). The explicit forall annotation on the bound and binding variable x causes the program to infer a Rank 2 polytype as indicated by the "-> Int" following the (forall a. a), while noting the absence of a type variable following the outer forall printed by the program, correct?

-- Example 12 - Another Universal Quantifier Annotation on Typed Abstraction, Rank 2
-- \(x::(forall a. a -> a)). x -- (\(x::(forall a. a -> a)). x) :: (forall b. (forall a. a -> a) -> b -> b) -- Also Rank 2, the universal quantifier on type variable b ranges over the type variable a as well as the polytype bs.

-- Example 13 - Yet Another Universal Quantifier Annotation on Typed Abstraction, Rank 2
-- (\(f::(forall a. a -> a)). \(x::(forall b. b)). f (f x)) :: (forall c. (forall a. a -> a) -> (forall b. b) -> c) -- This is still rank 2. Rank 3 requires another level of nesting.

-- Section 3 - Alpha, Beta and Eta reductions. Interesting examples of abstraction, application, lets and subsumption. 

-- Example 14 - Alpha reduction: (\X -> E) => (\Y -> E) [X := Y] , if Y not free in E. There are no free variables. Bound variables are renamed.
-- \x. \x. x -- (\x. \x. x) :: (forall a b. a -> b -> b)

-- Example 15 - Omega term not allowed
-- (\x. x x) (\x. x x ) -- Occurs check for '$1' in: $1 -> $2

-- Example 16 - Beta Reduction: (\V -> E) F => E [V := F] The application of the rand F to the rator (\V -> E) reduces to E where V is replaced by F.
-- (\x. x) (\x. x) -- ((\x. x) (\x. x)) :: (forall a. a -> a) -- degenerate case

-- Example 17 - More Examples of Explicit and implicitly Typed Beta Reduction
-- (\x. x) (\x. \y. y) -- ((\x. x) (\x. \y. y)) :: (forall a b. a -> b -> b) -- reduces to rand
-- (\(x::(forall a. a -> a)). x) (\x. x) -- ((\(x::(forall a. a -> a)). x) (\x. x)) :: (forall a. a -> a) -- Rank 2
-- ((\x. x) :: (forall a. a -> a)) (\(x::Int). x) -- (((\x. x) :: (forall a. a -> a)) (\(x::Int). x)) :: (forall. Int -> Int)
-- ((\(x::(forall a. a -> a)). x) (\x. x) -- (((\(x::(forall a. a -> a)). x) (\x. x)) :: (forall a. a -> a)) :: (forall a. a -> a)

-- Example 18 - Eta Reduction: (\X -> F X) => F, if X not free in F
-- \x. (\y. y) x -- (\x. (\y. y) x) :: (forall a. a -> a) -- degenerate case

-- Example 19 - More Examples of Eta Reduction with Explicit Type Annotations
-- \(x::forall a. a -> a). (\(y::forall b. b -> b). y) x -- (\(x::(forall a. a -> a)). (\(y::(forall b. b -> b)). y) x) :: (forall b. (forall a. a -> a) -> b -> b) -- Still Rank 2
-- \(x::Bool). (\y. y) 0 -- (\(x::Bool). (\y. y) 0) :: (forall. Bool -> Int)
-- \x. (\(y::Bool). y) 0 -- (\x. (\(y::Bool). y) 0) -- Cannot unify types: Int Bool
-- \(x::(forall a. a -> a)). (\y. y) x -- (\(x::(forall a. a -> a)). (\y. y) x) :: (forall b. (forall a. a -> a) -> b -> b)

-- Example 20 - Implicitly Typed Let with Equivalent Application: let V = F in E <=> (\V -> E') F
-- let x = 0 in x -- (let { x = 0 } in x) :: (forall. Int) -- (\x. x) 0 -- Rank 0

-- Example 21 - Another Implicitly Typed Let with Equivalent App
-- let x = \y. y in x -- (let { x = \y. y } in x) :: (forall a. a -> a) -- (\x. x) (\y. y) -- Rank 1

-- Example 22 - Explicitly Typed Let with Equivalent App
-- let x = 0 in x :: Int -- (let { x = 0 } in x :: Int) :: (forall. Int) -- (\(x::Int). x) 0 -- Rank 0

-- Example 23 - Explicitly Typed Let with Equivalent App
-- let x = \(y::forall a. a -> a) . y in x -- (let { x = \(y::(forall a. a -> a)). y } in x) :: (forall b. (forall a. a -> a) -> b -> b) -- (\(x::(forall a. a -> a)). x) - Rank 2

-- Example 24 - Explicitly Typed Let, Not Equivalent to Application
-- let x = \(y::Int). y in \(x::(forall a. a -> a)). x -- (let { x = \(y::Int). y } in \(x::(forall a. a -> a)). x) :: (forall b. (forall a. a -> a) -> b -> b) -- Rank 2
-- (\(x::(forall a. a -> a)). x) (\(y::Int). y) -- Cannot unify types: a 1 Int

-- let x = \(x::forall a. a -> a). x in \(y::Int). y -- (let { x = \(x::(forall a. a -> a)). x } in \(y::Int). y) :: (forall. Int -> Int) -- (\(y::Int). y) (\(x::(forall a. a -> a)). x) -- Cannot unify types: Int $0 -> $1

-- Example 25 - Explicitly Typed Let, Not Equivalent to Application 

-- let x = \(y::forall a. a -> a). y in \x. x -- (let { x = \(y::(forall a. a -> a)). y } in \x. x) :: (forall a. a -> a) -- ((\(x::(forall a. a -> a)). x) (\y. y)) :: (forall a. a -> a) -- Rank 1

-- let x = \y. y in \(x::forall a. a -> a). x -- (let { x = \y. y } in \(x::(forall a. a -> a)). x)  :: (forall b. (forall a. a -> a) -> b -> b) -- Rank 2 -- (\y. y) (\(x::forall a. a -> a). x) -- Subsumption check failed: $1 is not as polymorphic as (forall a. a -> a)

-- Restatement of Subsumption
-- the type of rand must be at least as (more) polymorphic as the rator, known as subsumption
-- contravariantly, s1 in the rator must be at least as polymorphic as s2 in the rand
-- if s1 is more polymorphic than s2, then t1 = (s1 -> Int) is less polymorphic than t2 = (s2 -> Int)

-- Example 26 - Explicitly Typed Rand Subsumes Rator
-- t1 = (\x. 0) :: (forall a. a -> Int) -- s1 = a
-- t2 = (\(x::Int). 0) :: (forall. Int -> Int) -- s2 = Int
-- s1 is more polymorphic than s2, therefore t1 is less polymorphic than, or subsumed by t2 and the following application succeeds
-- (\x. 0) (\(x::Int).x) -- ((((\x. 0) :: (forall a. a -> Int)) ((\(x::Int). 0) :: (forall. Int -> Int))) :: (forall. Int)) - Rank 0
-- (\(x::Int). 0)(\x. 0) -- Switch terms and Cannot unify types Int $4 -> $5

-- Example 27 - Explicitly Typed Rand Subsumes Rator, Rank Difference
-- (\(x::(forall a. a -> a)). x) (\x. x) -- (((\(x::(forall a. a -> a)). x) (\x. x)) :: (forall a. a -> a)) :: (forall a. a -> a) -- Rand at least as polymorphic as rator (s1 in rator is rank1, though rator is rank 2 and rand is rank 1)
-- (\x. x) (\(x::(forall a. a -> a)). x) -- Although rand is rank 2, Subsumption check failed: $1 is not as polymorphic as (forall a. a -> a)

-- Section 4 - Type Unification Errors

-- Example 30 - Typed Application, Explicitly Divergent Types
-- (\(x::Bool). x) (\x. 0) -- (\(x::Bool). x) ((\x. 0) :: (forall a. a -> Int)) -- Cannot unify types: Bool $2 -> $3
-- (\x. 0) (\(x::Bool). x) -- ((\(x::(forall a. a -> a)). x) (\x. x) (\x. 0) (\(x::Bool). x)) :: (forall. Int) -- Rank 0 and works, but the following does not, explain?
-- (\(x::Int). 0)(\(x::Bool). x) -- Cannot unify types: Int $0 -> $1

-- Example 31 - Typed Application, Implicitly Divergent Types
-- (\(x::Bool). 0)(\x. x) -- Cannot unify types: Bool $0 -> $1
-- (\x. x)(\(x::Bool). 0) -- ((\(x::(forall a. a -> a)). x) (\x. x) (\x. x) (\(x::Bool). 0)) :: (forall. Bool -> Int)

-- Example 31 - Typed Application, Implicitly Divergent Types
-- (\(x::a). x) (\x. 0) -- Panic! Unexpected types in unification: a $0 -> $1
-- (\x. 0)(\(x::a). x) -- Panic! Unexpected types in unification: $1 a

-- Example 32 - Typed Application, Explicitly Divergent Types
-- (\(x::Int). x)(\(x::(forall a. a -> a)). x) -- Cannot unify types: Int $0 -> $1
-- (\(x::(forall a. a -> a)). (\(y::Int). y) x) -- Cannot unify types: Int $1 -> $2 ***

-- Example 33 - Typed Application, Type Constant
-- (\(x::a). (\(y::a). y) x) -- Panic! Unexpected types in unification: a a
-- (\x. (\(y::a). y) x) -- Panic! Unexpected types in unification: $0 a
-- (\(x::a). (\y. y) x) -- Panic! Unexpected types in unification: a $0

-- Section 5 - List terms and the explicitly quantified principle types derived from the terms. Using application and beta reduction show the principle type of terms. One can also use ghci to evaluate these terms.

-- Example 34 - Deriving Various Implicit Terms and Their Principle Types

-- deriving various terms with Int
-- (\x. 0) :: (forall a. a -> Int) -- equivalently in ghci :t  (\x -> 0) :: Num a => t -> a
-- (\x. x 0) :: (forall a. (Int -> a) -> a)
-- (\x. x) :: (forall a. a -> a)

-- (\x. \y. x) :: (forall a b. b -> a -> b)
-- (\x. \y. y) :: (forall a b. a -> b -> b)
-- (\x. \y. x y) :: (forall a b. (a -> b) -> a -> b)
-- (\x. \y. y x) :: (forall a b. a -> (a -> b) -> b)
-- (\x. \y. x (y x)) :: (forall a b. (a -> b) -> ((a -> b) -> a) -> b)
-- (\x. \y. y (x y)) :: (forall a b. ((a -> b) -> a) -> (a -> b) -> b)

-- (\x. \y. x 0) :: (forall a b. (Int -> b) -> a -> b)
-- (\x. \y. y 0) :: (forall a b. a -> (Int -> b) -> b)
-- (\x. \y. x y 0) :: (forall a b. (a -> Int -> b) -> a -> b)
-- (\x. \y. y x 0) :: (forall a b. a -> (a -> Int -> b) -> b)
-- (\x. \y. y (x 0)) :: (forall a b. (Int -> a) -> (a -> b) -> b))
-- (\x. \y. x (y 0)) :: (forall a b. (a -> b) -> (Int -> a) -> b)

-- \x. \y. x x 0 -- Occurs check for '$2' in: $2 -> $3
-- \x. \y. y y x 0 -- Occurs check for '$2' in: $2 -> $3

-- (\x. \y. y (y 0)) :: (forall a. a -> (Int -> Int) -> Int)
-- (\x. \y. x (x 0)) :: (forall a. (Int -> Int) -> a -> Int)

-- (\x. \y. y (x (x 0))) :: (forall a. (Int -> Int) -> (Int -> a) -> a)
-- (\x. \y. x (y (y 0))) :: (forall a. (Int -> a) -> (Int -> Int) -> a)

-- note type variable dropped
-- (\x. \y. y (x (y (y 0)))) :: (forall. (Int -> Int) -> (Int -> Int) -> Int)
-- (\x. \y. x (y (x (x 0)))) :: (forall. (Int -> Int) -> (Int -> Int) -> Int)

-- (\x. \y. \z. 0) :: (forall a b c. a -> b -> c -> Int)

-- application
-- ((\x. \y. x) (\x. x)) :: (forall a b. a -> b -> b)
-- ((\x. \y. y) (\x. x)) :: (forall a. a -> a)

-- ((\x. \y. y) (\x. \y. x)) :: (forall a. a -> a)

-- ((\x. \y. x) (\x. \y. x)) :: (forall a b c. a -> c -> b -> c)
-- ((\x. \y. x) (\x. \y. y)) :: (forall a b c. a -> b -> c -> c)

-- ((\x. \y. y x) (\x. \y. y x)) :: (forall a b c. ((a -> (a -> b) -> b) -> c) -> c)

-- Beta Reduction: (\V -> E) F => E [V := F] The application of the rand F to the rator (\V -> E) reduces to E where V is replaced by F.
-- a few sample terms

-- #1
-- (\x. \y. x) (\x. x) => substitute
-- (\x. \y. (\x. x))   => reduce
-- \y. \x. x	       => alpha rename
-- (\x. \y. y) :: (forall a b. a -> b -> b)

-- #2
-- ((\x. x) (\x. \y. y x)) => substitute
-- (\x. (\x. \y. y x)) 	   => reduce
-- (\x. \y. y x) :: (forall a b. a -> (a -> b) -> b)

-- #3
-- (\x. \y. x y) (\x. x)      => substitute
-- \x. \y. ((\x. x) (\y. y))  => reduce
-- (\x. x)  :: (forall a. a -> a)

-- #4
-- (\x. \y. x y) (\x. \y. y x)		 => substitute
-- \x. \y. ((\x. \y. y x) (\x. \y. y x)) => reduce
-- (\x. \y. y x) (\x. \y. y x) 	     	 => ? not normal form?
-- (\x. \y. y x) :: (forall a b. a -> (a -> b) -> b)

-- Section 6 - Adding Explicit Quantifiers Results in a Change of Principle Type

-- Example 35 - Type Variables with Arguments Reversed Plus New Quantifier (C)

-- (\x. \y. x) :: (forall a b. b -> a -> b)
-- (\(x::(forall a. a)). \(y::(forall b. b)). x) :: (forall c. (forall a. a) -> (forall b. b) -> c)

-- Example 36 - Function Argument Missing

-- (\x. \y. y x) :: (forall a b. a -> (a -> b) -> b)
-- (\(x::(forall a. a -> a)). \(y::(forall b. b -> b)). y x) :: (forall c. (forall a. a -> a) -> (forall b. b -> b) -> c -> c)

Haskell Terms and Types

{-# LANGUAGE RankNTypes, DatatypeContexts, ExistentialQuantification #-}
-- http://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types
-- A Direct Algorithm for Type Inference in the Rank 2 Fragment of the Second-Order Lambda-Calculus
-- Practical Type Inference For Arbitrary Rank Types
-- http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.46.4938&rep=rep1&type=pdf
-- http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.95.2624&rep=rep1&type=pdf
-- http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.22.2695&rep=rep1&type=pdf

-- can ghci evaluate explicitly typed terms
-- terms are admissible whose explicitly quantified types are admissible
-- explicit quantifiers and principle types

module Main where

-- Section 1, basics

-- Example 1 - Literal

e1 :: Int -- implicitly quantified, rank 0
e1 = 0

e1' :: forall. Int -- explicitly quantified, rank 0
e1' = let
	  g :: Int -> Int -- implicitly quantified, rank 0
	  g x = x
       in g 0

-- Example 2 - Explicitly Quantified, Monomorphic Type

e2 :: forall. Int -> Int -- explicitly quantified, rank 0
e2 x = x

-- e2' :: forall. a -> a -- Main.hs:45:22: Not in scope: type variable `a', ? no type constants
-- e2' x = x

-- Example 3 - Explicitly and Implicitly Quantified Polytype

e3 :: a -> a -- implicitly quantified, rank 1
e3 x = x

e3' :: forall a. a -> a -- explicitly quantified, rank 1
e3' x = x -- e3 0 0 it :: Integer

-- Example 4 - Explicitly Quantified Polytype, rank 2

e4 :: (forall a. a -> a) -> Int -- explicitly quantified, rank 2
e4 x =  x 0

-- type constructors, implicit quantifier, rank 2

-- | No explicit universal quantifier
data T a = TC0 a | TC1 Int | TC2 (a -> a) | TC3 (Int -> Int)

-- :kind! T -- T :: * -> *
-- :t TC0 :: a -> T a
-- :t TC1 -- TC1 :: Int -> T a
-- :t TC2 -- TC2 :: (a -> a) -> T a
-- :t TC3 -- TC3 :: (Int -> Int) -> T a

-- the expressions below are not meant to be printed
-- evaluate the expressions and get the message to implement show
-- check the types of each using :t on the type constructor
-- check the kind using :kind! on the type

-- Example 6 - Monomorphic Type Variable Allows Any Monomorphic Type
e6 :: T Int -- notice the type is NOT (T a)
e6 = TC0 0

e6' :: T Bool -- same as above
e6' = TC0 True

e6'' :: T (a -> a)
e6'' = TC0 ((\x y -> x (x y)) (\y -> y))

-- Example 7 - Monommorphic Type Restriction (Int)
e7 :: T a -- notice the type IS (T a)
e7 = TC1 0

-- e7' = TC1 True -- Couldn't match expected type `Int' with actual type `Bool'

-- Example 8 - Monomorphic Function on Type Variables (a -> a), Function Evaluation
iid :: Int -> Int
iid x = x

bid :: Bool -> Bool
bid x = x

e8 :: T Int -- although the type is TC2 :: (a -> a) -> T a, the type system infers T Int
e8 = TC2 iid

e8' :: T Bool -- same
e8' = TC2 bid

-- e8'' = TC2 0 -- No instance for (Num (a0 -> a0))

-- Example 9 - Monomorphic Function on Type Restriction (Int -> Int), Function Evaluation
e9 :: T a -- although the type constructor is TC3 :: (Int -> Int) -> T a, the type system infers T a
e9 = TC3 iid

e9' :: T a -- more general types are allowed (id)
e9' = TC3 id

-- e9'' = TC3 bid -- Couldn't match expected type `Int' with actual type `Bool' Expected type: Int -> Int Actual type: Bool -> Bool

-- e9''' = TC3 ((\x y -> x (x y))) -- The lambda expression `\ x y -> x (x y)' has two arguments, but its type `Int -> Int' has only one

-- Example 10 - Existential (Union) Type

-- It would appear that U has one type constructor with an explicitly quantified type: UC1, however the universal quantifier does not appear in either of these existentially quantified types. Because there is no universal quantifier these would be considered rank 0 types and the type variable in UC1 would be inhabited by monomorphic types.

data U = forall a. UC1 a | forall. UC2 Int

-- :kind! U :: *
-- :t UC1 :: a -> U1 -- note no universal quantifier
-- t: UC2 :: Int -> U1 -- note no universal quantifier, no type variable

e10 :: [U] -- existential type
e10 = (UC1 0) : [UC1 True]

-- e10' = UC2 True -- Couldn't match expected type `Int' with actual type `Bool'

-- Example 11 Explicitly Quantified (Intersection, Identity and Multiparam) Types, Rank 2

-- These explicitly quantified type constructors are all rank 2. 

data U1 = UC1' (forall a. a) | UC2' (forall a. a -> a) | UC3' (forall a b. a -> b -> b)

-- :kind! U1 :: *
-- :t UC1' :: (forall a. a) -> U1
-- :t UC2' :: (forall a. a -> a) -> U1
-- :t UC3' :: (forall a b. a -> b -> b) -> U1

e11 :: U1
e11 = UC1' undefined -- only undefined is admissable under this type because it is the intersection of all types

e11' :: U1 -- only matching polytypic type variables are accepted, as below monomorphic types are rejected by the type system
e11' = UC2' id

e11'' :: U1 -- and terms that reduce to the principle type are admissible
e11'' = UC2' ((\x y -> x y) (\x -> x))

-- e11'' application and beta reduction
-- (\x. \y. x y) (\x. x)      => substitute
-- \x. \y. ((\x. x) (\y. y))  => reduce
-- (\x. x)  :: (forall a. a -> a)

-- e11''' = UC2' bid -- Couldn't match type `a' with `Bool' `a' is a rigid type variable bound by a type expected by the context: a -> a 

-- e11'''' = UC2' 0 -- No instance for (Num (a -> a)) arising from the literal `0'

e11''''' :: U1 -- matching polyptypic types are accepted
e11''''' = UC3' (\x y -> y) -- :: (forall a b. a -> b -> b)

-- e11'''''' = UC3' (\x y -> x) -- nonmatching are rejected - Couldn't match type `a' with `b' `a' is a rigid type variable bound by a type expected by the context: a -> b -> b at Main.hs:159:12   `b' is a rigid type variable bound by a type expected by the context: a -> b -> b at Main.hs:159:12

-- e11'''''' = UC3' ((\x -> x) (\x y -> y x)) -- Couldn't match type `b' with `a -> b' `b' is a rigid type variable bound by a type expected by the context: a -> b -> b at Main.hs:165:8

-- e11'''''' application and beta reduction explains this mismatch
-- ((\x. x) (\x. \y. y x)) => substitute
-- (\x. (\x. \y. y x)) 	   => reduce
-- (\x. \y. y x) :: (forall a b. a -> (a -> b) -> b)

-- Example 12 - Covariant (?) and Contravariant Explicitly Quantified Type Constructors

-- UC4 is a rank 2 type constructor noting that the right parenthese around forall b. b -> b are removed when checking its type. UC4' is a rank 3 type constructor, noting the type checker perserves the parentheses around (forall b. b -> b).

data U4 = UC4 (forall a. a -> (forall b. b -> b)) | UC4' (forall a. (forall b. b -> b) -> a)

-- :kind! U4 :: *
-- :t UC4 :: UC4 (forall a. a -> forall b. b -> b) -> U4
-- :t UC4' :: (forall a. (forall b. b -> b) -> a) -> U4

e12 :: U4
e12 = UC4 (\x y -> y) -- matches parameters

e12' :: U4
e12' = UC4 ((\x y -> x) (\x -> x)) -- reduction

-- beta reduction on term in type constructor
-- (\x. \y. x) (\x. x) => substitute
-- (\x. \y. (\x. x))   => reduce
-- \y. \x. x	       => alpha rename
-- (\x. \y. y) :: (forall a b. a -> b -> b)

-- what are the implicit terms that are admissible by the type
-- what is the method for determining
-- given a term what is are the principle type(s) among choices of the explicit quantifiers
-- what is a term of rank n that is admissible by the principle type
e12'' :: U4
e12'' = UC4' undefined -- see section 6 in Tc monad

-- Example 13

-- The first type constructor is rank 2, the second, third and fourth type constructors are rank 3. The implicit terms are admissible when their explicitly quantified principle type is admissible. See section 5 and 6 in Tc monad.

data U5 = UC5 (forall a. a -> Int) | UC5' ((forall a. a -> a) -> Int) | UC5'' ((forall a. a -> a) -> (forall b. b -> b) -> Int) | UC5''' (forall b. (forall a. a -> a) -> b -> b)

-- :kind! U5 :: *
-- :t UC5 :: (forall a. a -> Int) -> U5
-- :t UC5' :: ((forall a. a -> a) -> Int) -> U5
-- :t UC5'' :: ((forall a. a -> a) -> (forall b. b -> b) -> Int) -> U5
-- :t UC5''' :: (forall b. (forall a. a -> a) -> b -> b) -> U5

-- terms are admissible whose explicitly quantified types are admissible
-- (\x -> 0) :: Num a => t -> a
-- (\x. 0) :: (forall a. a -> Int)
e13 :: U5
e13 = UC5 (\x -> 0) 

-- (\x -> x 0) :: Num a => (a -> t) -> t
-- explicitly quantify x with forall a. a -> a
-- (\(x::(forall a. a -> a)). x 0) :: (forall. (forall a. a -> a) -> Int)
e13' :: U5
e13' = UC5' (\x -> x 0) 

-- (\x. \y. y (x 0)) :: (forall a b. (Int -> a) -> (a -> b) -> b)
-- explicitly quantify x with forall a. a -> a and y with forall b. b -> b
-- (\(x::(forall a. a -> a)). \(y::(forall b. b -> b)). y (x 0)) :: (forall. (forall a. a -> a) -> (forall b. b -> b) -> Int)
e13'' :: U5
e13'' = UC5'' (\x y -> y (x 0))

-- By inspection the implicitly typed term (\x. \y. y) infers the principle type (forall a b. a -> b -> b), so that term is admissible in UC5''' as would it be with (forall b. (forall a. a) -> b -> b) where the universally quantified type variable a has been reduced from a function.

e13''' :: U5
e13''' = UC5''' (\x y -> y) -- the term (\x -> x) is also admissible here ...

-- Example 14 - Contravariant Type Constructors, Rank 3 and Rank 5

data U6 = UC6 (forall b. (forall a. a -> b) -> b) | UC6' ((forall c. (forall b. (forall a. a -> a) -> b) -> c) -> Int)
-- :kind! U6 :: *
-- :t UC6 :: (forall b. (forall a. a -> b) -> b) -> U6
-- :t UC6' :: ((forall c. (forall b. (forall a. a -> a) -> b) -> c) -> Int) -> U6

-- inspection should be replaced by a system in which we infer the admissible principle type from the implicitly typed terms. See section 6 in the accompanying Tc Monad.

In Search of a Paradigm: The Science of Methods

Regular readers of the Phaneron may consider this essay as a departure from the usual subjects discussed here, those being of philosophy, logic, semiotics and singularity. However, the astute reader will recognize the close association between the subject of this essay and the philosophy of science.

2012 was a year where I took the opportunity to focus on methods. Methods have been an interest of mine for most of my career. This interest lead to my certification in the Rational Unified Process, SCRUM Master and the Software Engineering Institute’s CMMI-DEV. Late in 2011 I became active in the Theory Track of Ivar Jacobson’s Software Engineering Method and Theory (SEMAT) initiative. My work on the Theory Track motivated me to engage the US Federal CIO Council’s Management Best Practices Committee to establish an Agile Practices Working Group and to become an affiliate in the Software Engineering Institute‘s Affiliate Program. Although my motivations were practical, I believe the result of this year’s focus is more than that. I believe the result is significant. What’s significant is that I can now articulate a problem statement that has perplexed me and I suspect many of us in software for the past few decades. In the rest of this essay, I will begin with a situation analysis derived from a few informal Theory Track discussions, then explain the problem statement. Following from the problem statement, I’ll propose the hypothesis that software engineering doesn’t need another method, it needs a science of methods, then I will describe how we as software engineers should analyze and reason about methods.

Before I begin, I want to thank Pontus Johnson for the thoughtful email discussion. I also want to thank Ivar Jacobson for his leadership in creating the environment where a such a discussion can take place. There are few opportunities to have this type of discussion. The workplace is generally not one. So many thanks to Ivar. For those of us lucky enough to work with him, his selfless leadership is as much a part of his legacy as his many accomplishments.

I’ll begin by framing our situation analysis in terms of the following questions: Have you ever wondered why software engineering has so many methods? And have you wondered why none of the proposed methods can be conclusively shown to improve, serve as an complete explanation for and consistently avoid regularly recurring failures on software projects? Do you find it unsatisfactory that our profession encourages certain practitioners to propose a method while at the same time hold that this same method cannot be defined or its practices independently verified? Have you questioned whether what we as software professionals really face is a trade off between a metaphorical cathedral and a bazaar? Have you ever thought that you’re not really looking for a silver bullet, just a known approach you can recommend to a senior executive without later finding both unexplainable cost overruns and collateral damage to your reputation? Is it that we just haven’t found the right method and that one’s just around the corner? If you’ve asked yourself these questions, then you’ve asked yourself something fundamental about the state of our profession.

It was 1970 when Winston Royce published Managing the Development of Large Software Systems. Although new methods have been proposed since, there’s little evidence that any of the methods proposed are responsive to the questions posed in our situation analysis. No doubt we’ve had the time. I count 42 years since 1970. And we’ve engaged in a certain kind of institutional research – the Software Engineering Institute has been around for 25+ years – as well as non-institutional approaches which claim to be based on empiricism or meritocracy. The results are underwhelming. Failure of software projects is still too much the norm, especially here in Washington, DC. And both high cost and risk still too often characterize the environment in which we work. In short, we’re in a do loop and just to develop a problem statement from our situation analysis, we need a different perspective if we expect a different result than what we have so far.

Thomas Kuhn’s Structure of Scientific Revolutions was required reading in my high school and I’ve had a copy in my bookshelf ever since. Very early in the development of SEMAT, Ivar Jacobson posed the question: Where are Maxwell’s Equations for Software Engineering? I believe this an excellent question and one that with some refinement helps frame the problem statement following from our situation analysis. Ivar’s question also implicitly formulates the hypothesis that a paradigm can, but does not yet exist for software engineering. I have challenged this hypothesis in the Theory Track discussions. Research on the legitimacy of paradigms in the social sciences remains inconclusive. The interested reader will enjoy the Preface to the Second Edition and its Postscript as well as the Stanford Encyclopedia of Philosophy article on Scientific Revolutions.

Distinguished sociologist Charles Tilley pessimistically says here that “The social sciences have never developed as connected a body of knowledge [as the natural sciences], integrated with a set of procedures for verifying that knowledge and the social sciences have remained a contested terrain and that’s something people often try to articulate incorrectly …” Kuhn chooses to write exclusively about the natural sciences in the Structure of Scientific Revolutions. In the chapter called the Route to Normal Science, Kuhn says that it is an open question whether “parts of social science have yet acquired such paradigms at all.” Unfortunately, Kuhn does not elaborate on what parts of the social sciences may or may not have formulated paradigms. If even Kuhn leaves doubt whether social sciences have formulated paradigms, then what of software engineering? It is unlikely that we will find the natural laws of software engineering. And it would be optimistic to conclude that software engineering as we practice it today is a social science. To equate software engineering with the natural sciences would both be an error and set an indirect course for a science of methods.

Our problem statement then is this: If we cannot expect to formulate a paradigm for software engineering as one might expect from a natural science, or more optimistically a social science, must it remain nothing more than social engineering? If we require more than social engineering in response to our situation analysis, is a paradigm necessary for a science of methods? If a paradigm is not necessary, what is a science of methods and what are its minimal parts?

I believe many, if not all, software engineers would endorse the belief that software engineering needs more than social engineering in response to our situation analysis. There are no shortage of people who are not software engineers who would not. I will count general managers who lack experience in software who believe they can manage anything, venture capitalists who believe they can slide a pizza box under a locked door and have a multi-million dollar application appear just in time to execute an exit strategy, those who believe they are the next Mark Zuckerberg, and quick and dirty civic hackers who believe they can compete on a $100 million project, to name just a few. Those who believe software engineering should remain nothing more than social engineering require us all to accept less from ourselves than what we might expect from a physician, lawyer, accountant or plumber. We expect more than social engineering from others and we should expect it from ourselves.

Good news. A paradigm is not necessary for a science of methods. Those who read the Scientific Revolutions article in the Stanford Encyclopedia of Philosophy know there are competing theories of scientific analysis. This comment is not to minimize Kuhn’s work, but to recognize diversity in the history and philosophy of science as well as remove the dependency on only one of those theories in developing a science of methods.

So what is a science of methods? Simply put, a science of methods is the application of the scientific method to software engineering. That’s a pretty simple definition and I’ll just say these three things about it. 1) With all this talk about science I do not mean to minimize the social aspects of teaming. I mean that without science, the social aspects are not sufficient. 2) When we talk about a theory of software engineering on the SEMAT Theory Track we separate software engineering from computer science as two distinct subject areas. 3) We do not expect that the science of methods will find the missing method, the method of all methods, or the meta-method. There’s no one method, just like there’s no one ring. I want to take the opportunity to endorse the good work of SEMAT, both its proposal that methods are a composition of practices and the development of a kernel of practices, from which methods can be composed. I believe this work is consistent with a science of methods. I also think the natural follow-on to the current SEMAT activities is how to analyze and reason about methods composed from practices in the kernel.

Analyzing methods and reasoning about methods are the minimal parts of the science of methods. I will mention a few other desirable parts below. I make no attempt to provide an ontology of the science of methods. The effort to bound that analysis might be longer than the current essay. I will limit the analysis of methods to the qualities of methods that allow us to judge their nature whether having to set them in relation to, or remain independent of something else. It is not that a method is invalid if it fails to satisfy these qualities. More importantly we recognize the method for those qualities it possesses rather than avoid acknowledging the strengths and weaknesses of a method. The qualities also help us in composing practices from the kernel. So, the qualities are as follows:

  1. Sound. A method is sound if it is not inconsistent. Inconsistent means the method contains contradictory statements.
  2. Complete. A method is complete if it is not missing something. We leave the boundary problem undefined.
  3. Intentional. A method that is intentional has and is aligned with a purpose. We leave the purpose undefined.
  4. Parsimonious. A method that is parsimonious has no extra statements. We allow for synonyms in the terms.
  5. Falsifiable. A method that contains statements that are not falsifiable – true or false – is ambiguous. This is SEMAT Principle #6.
  6. Objective. A method that is objective both contains only statements whose criteria for falsifiability and method of reasoning are defined. This is a little more than SEMAT principle #12.

I define reasoning about methods in terms of reaching a conclusion based on premises in the usual way one would expect from logic. The science of methods allows for the already well known subjects of deduction, induction and abduction. While allowing these broad categories of logics in reasoning about methods, we also require a statement of the proof theory under which the conclusion was reach from the premises. For those not familiar with abduction, abduction is evidence that a is necessary but not sufficient to conclude b. The science of methods also allows the weaker notion of indication by John W. Tukey. Tukey’s observations on indication, determination and inference provide a practical approach to reason under uncertainty. When we reason about a method using indication, we expect the acknowledgement of which proof theory and its provenance allowed reaching the conclusion.

With the minimal parts of the science of methods defined, I remain pragmatic and acknowledge that experimentation is a desired part of the science of methods to be defined later. No doubt industrial research promises empirical results from experimentation, but isolating controlled variables in a industrial setting remains a significant challenge in most if not all research into software engineering practices. There may also be other desired parts later defined.

Some 42 years after Winston Royce published Managing the Development of Large Software Systems we are still in search of a paradigm. It’s unlikely we’ll find one like the natural sciences, but with the excellent foundation provided by SEMAT I have defined here the minimal parts of a science of methods. The science of methods does not preclude social engineering in software engineering. We simply ask from ourselves, what we’d ask from others.

In later posts I will describe my recent experiences with the Software Engineering Institute and the CIO Council examining “agile practices” for the US Federal government. I will apply the science of methods to claims about methods in general and analyze reports and guidance from certain unidentifed “state actors.”

Down the Rabbit-Hole with Monad Transformers

My experience with Haskell has been all about rabbit-holes. This one was not quite so scary as what Alice experienced. There was no watch or waist coat pocket. The tunnel didn’t seem like a very deep well and I always knew where to find bottom. That’s a good sign. It was not always that way.

I had taken an interest in type families and was working my way through Fun with Type Functions. I saw an expression and wondered,  What can I actually do with that? It was at that point that I decided to go down the rabbit-hole with monad transformers.

I haven’t yet returned to that expression, but I picked up something on the way down and brought it back.

{-# LANGUAGE NoMonomorphismRestriction, DatatypeContexts, FlexibleContexts, FlexibleInstances #-}
-- http://en.wikibooks.org/wiki/Haskell/Monad_transformers
-- http://www.cs.nott.ac.uk/~nhn/MGS2006/LectureNotes/lecture03-9up.pdf

module Main where

import Control.Monad
import Control.Monad.Trans.Class

-- |A parameterized type I representing an "inner type" with one constructor IC
data I a = IC a deriving (Show)

-- |Unwraps the value in the type I
unI (IC x) = x

-- |A parameterized new type O m a representing an "outer type" with a named constructor
newtype (Monad m) => O m a = OC { runO :: m (I a)}

-- uses runO to unwrap x into an m (I a) computation
-- v <- runO x extracts an I a value v
-- unI v extracts the value in a
-- f (unI v) applies the function to the (I a) value
-- runO (f (unI v)) executes f value in O m a, since f has type O m a as a result type
-- do block has type m (I a) it's wrapped in O m a constructor

-- |A monad transformer instance on type O m a
instance Monad m => Monad (O m) where
 return = OC . return . IC
 x >>= f = OC $ do { v <- runO x; runO (f (unI v))} -- the type of x is (O (I a))   

-- an alternative bind closely resembling the references above
-- x >>= f = OC $ do { v <- runO x; case v of IC value -> runO $ f value}

-- uses runO to unwrap x into an m (I a) computation
-- extracts an I a value v
-- case v of IC value allows pattern match on a, the value
-- apply f to a, the value, aka ... applies f to the I a value ...
-- since f has type O m a as a result type, runO executes f value in O m a
-- do block has type m (I a) it's wrapped in O m a constructor

-- a similar example that
-- uses new type on the inner type
-- unwraps O m a

-- |A parameterized new type I' representing an "inner type" with one constructor IC'
newtype I' a = IC' a -- deriving (Show)

-- |Unwraps the value in the inner type
unI' (IC' x) = x

-- |A monad instance on the inner type
instance Monad I' where
 return = IC'
 m >>= f = f (unI' m)

-- | A show instance of I' a
instance Show a => Show (I' a) where
 show (IC' x) = "IC' " ++ show x

-- |Witness on inner type
w :: Num a => I' a
w = (IC' 0) >>= return . id

-- |A parameterized new type O' m a representing an "outer type" with a named constructor
newtype O' m a = OC' {runO' :: m (I' a)} -- deriving (Show)

-- | A Show instance of O' I' a
instance Show a => Show (O' I' a) where
 show (OC' x) = "OC' " ++ show (unI' x)

-- |Unwraps the value in the outer type
unO' (OC' (IC' a)) = a

-- uses runO' to unwrap x into an m (I' a) computation
-- v <- runO' x extracts an I' a value v
-- unI' v extracts the value in a
-- f (unI' v) applies the function to the (I' a) value
-- runO' (f (unI' v)) executes f value in O' m a, since f has type O' m a as a result type
-- do block has type m (I' a) it's wrapped in O' m a constructor

-- |A monad transformer instance on type O' m a
instance Monad m => Monad (O' m) where
 return = OC' . return . IC'
 m >>= f = OC' $ do {v <- runO' m; runO' (f (unI' v))}

-- | Witness on monad transformer
w' :: Num (I' a) => O' I' a
w' = (OC' (IC' 0)) >>= return . id

-- | An Num instance lifted into I'
instance Num a => Num (I' a) where
 fromInteger x = IC' (fromInteger x)

-- lifting, liftM executes a function in a monad, lift executes the monad

-- | Executes addition on the zero in IC'
w'' :: Num a => I' a
w'' = liftM (+1) (IC' 0)

-- |Instance of monad transformer lifts m into O' m a
instance MonadTrans O' where
 lift m = OC' (m >>= return . IC')

-- |Executes addition on the zero in IC' and lifts the monad into O' m a
w''' :: (Num a) => O' I' a
w''' = lift ((IC' 0) >>= return . (+1))