COMP3161/9164 Concepts of Programming Languages
Term 3, 2025

Code and Notes (Week 9 Thursday)

Table of Contents

These are the extra notes and code I presented in today's lecture. Many thanks to Johannes Åman Pohjola for the original.

1. Notes

Three types of polymorphism
---------------------------

- parametric polymorphism
   (abstract from specific types w/ variables ranging over types)

   [Int]
   [Float]

   append :: forall a. [a] -> [a] -> [a]
     *same* implementation regardless of a

- ad-hoc polymorphism (overloading) 
   the feature that lets you write + for both int addition
   and float addition

   1 + 2 :: Int
   3.4 + 6.7 :: Float

   a -> a -> a
     *different* implementation for Int vs Float

- subtype polymorphism
   the feature that lets you treat a Dog as an Animal in Java

    class Animal {}
    class Cat extends Animal {}
    class Dog extends Animal {}


Extending MinHS with type classes
---------------------------------

Having constraints only on the polytypes means we won't allow this:

    x :: a -> (Num a => a)

Only on the outer level, like:

    x :: Num a => a -> a 

:info Num

Here's an example of what you'd find in axiom schema set A:

    {Num Word, Num Integer, Num Int, Num Float, Num Double}


Typing Rules for Overloading
----------------------------

Pass-through of A by existing rules:

    A|Γ ⊢ e1 : τ1       A|Γ ⊢ e2 : τ2
   _______________________
     A|Γ ⊢ (e1,e2) : τ1 × τ2

Using instantiation rule to eliminate typeclass Num constraint:

     A | Γ ⊢ e : Num Int ⇒ Int      A |⊢ Num Int
    _____________________________________________ Inst
             A | Γ ⊢ e : Int

Using generalisation rule to introduce typeclass Num constraint:

         Num a, A | Γ ⊢ double : a -> a 
        _________________________________ Gen
         A | Γ ⊢ double : Num a ⇒ a -> a


Partial order
-------------

  A relation R is a partial order if:

  Transitive:

     x R y   ∧   y R z   ⇒ x R z

  Reflexive

     x R x

  Anti-symmetric:

     x R y  ∧  y R x   ⇒ x ≠ y

For subtyping:

  class Siamese extends Cat

  class Cat extends Animal
  // we would like a Siamese   to count as an Animal --> transitivity
  // reflexivity: we would like a Siamese to count as a Siamese

  // anti-symmetry: no cycles in the subclass hierarchy

2. Haskell code

module W9B where

{- Overloading -}

{-
  ghci> :t (+)
  (+) :: Num a => a -> a -> a

  (+) has type a -> a -> a
    for every type that is a member of the class Num
 -}

-- Here's a function that works for types a
-- that satisfy typeclass constraint Num a
double :: Num a => a -> a
double x = x + x

-- Let's make our own datatypes an instance of Num, too!
data Fruit = Apple | Banana
  deriving Eq
  -- deriving (Eq,Show)
  -- deriving Show
-- ^ uses Haskell's default implementation for Show's methods

-- `:info Num` will tell you typeclass Num's methods
-- and here's how you can implement them manually:
instance Num Fruit where
  _ + _ = Apple
  _ * _ = Banana
  f1 - f2 = f2
  negate f = f
  abs f = Apple
  signum f = Banana
  fromInteger _ = Apple

-- `:info Num` will tell you similarly for Show,
-- and also can implement Show's methods manually:
instance Show Fruit where
  show Apple = "Apfel"
  show Banana = "Banane"

-- Haskell will try to infer the most general type class constraints
-- my_thing :: (Eq a, Num a) => a -> Bool
my_thing x =
  x + x == x

-- You can define your own typeclass like this:
class Sized a where
  size :: a -> Int

-- Here are a few instances for it:
instance Sized Bool where
  size True = 1
  size False = 0

instance Sized Int where
  size x = x

-- Generative instance -- more on this later
-- instance Sized a => Sized [a] where
--   size xs = sum (map size xs)

-- This should work for all the above instances
doubleSize :: Sized a => a -> Int
doubleSize x = 2*size x

{- What the type class constraint
      Sized a
   means is:

    a is a type with a size function defined.

   So: why not just pass the size function
    as an extra argument?
 -}

-- Now this is parametric polymorphism.
-- The first argument is the type for dictionaries
-- of the "size" typeclass:
doubleSize' :: (a -> Int) -> a -> Int
doubleSize' size x = 2*size x

-- the dictionary for `instance Sized Bool` would look like this
sizeBool :: Bool -> Int
sizeBool True = 1
sizeBool False = 0


{- Static dispatch doesn't work for polymorphic recursion -}

-- not polymorphic recursion
data MyList a = MyNil | MyCons a (MyList a)

-- polymorphic recursion: no good for static dispatch
-- (inlining of typeclass dictionary calls), because
-- you'd need unboundedly many dictionaries...
data Thing a =
  T (Thing [a])


{- Subtyping and its interaction with constructors -}

{- For product types:
 - Assuming Int <= Float,

         (Float,Float)
        /          \
       /            \
 (Float,Int)       (Int,Float)
       \          /
        \        /  Example below
          (Int,Int)

Well this seems to be right?

    (Int,Int)  <= (Int,Float)

But why?
  -}

-- The fact that Int <= Float is represented by the following
-- coercion function existing:
coerce :: Int -> Float
coerce = undefined -- well, the specific definition doesn't matter,
                   -- but it has to exist

-- Using that coercion, we get this one:
coerceII2IF :: (Int,Int) -> (Int,Float)
coerceII2IF (i1,i2) = (i1,coerce i2)

{- and similarly, we can get the other four edges.
 - but there's no relation between (Float,Int) and (Int,Float)! -}

-- We can also get this kind of hierarchy for sum types, e.g.
coerceII2IF' :: Either Int Int -> Either Int Float
coerceII2IF' (Left n) = Left n
coerceII2IF' (Right n) = Right(coerce n)
-- and so forth.

something :: (Float -> Int) -> (Float -> Float)
something f = \x -> coerce (f x)

something2 :: (Float -> Float) -> (Int -> Float)
something2 f = \x -> f (coerce x)
             -- x :: Int
                  -- f :: Float -> Float

somethingElse :: (Float -> Int) -> (Int -> Float)
somethingElse f = \x -> coerce $ f $ coerce x


{- Coercing a function between these types:

    Int -> Int

    Int -> Float

    Float -> Int

    Float -> Float

   Between which of these can we coerce, and
   when do we apply `coerce :: Int -> Float`?
 -}

-- Contravariance
-- Originally we had Int <= Float, now we have:
-- (Float -> Int) <= (Int -> Int)
coerceFun :: (Float -> Int) -> (Int -> Int)
coerceFun f = \n -> f(coerce n)

-- Covariance
-- Originally we had Int <= Float, now we have:
-- (Int -> Int) <= (Int -> Float)
coerceFun' :: (Int -> Int) -> (Int -> Float)
coerceFun' f = \n -> coerce(f n)

{-
 Covariance:
  - the relationship between the argument type(s)
    is the same as the relationship between the composite types
 Contravariance:
  - the relationship between the argument type(s)
    is the inverse of the relationship between the composite types
 -}

3. Java code

3.1. Liskov substitution principle

This (maybe a little cheap) example is meant to illustrate the impossibility of fully complying with the Liskov substitution principle in Java. 

class Animal {}

class Cat extends Animal {}

class Dog extends Animal {}

public class Liskov {
    public static void main(String [] args) {
        // This prints "class Dog"
        System.out.println((new Dog()).getClass().toString());
        // This prints "class Animal"
        System.out.println((new Animal()).getClass().toString());
        // Checkmate, Java proponents!
    }
}

3.2. Unsound covariance of arrays

The basic arrays in Java are covariant, allowing the following: 

class Animal {}

class Dog extends Animal {}

class Cat extends Animal {}

public class Dog2Cat {
    public static Cat dog2cat(Dog dog) {
        Cat[] cats = new Cat[10];
        // Only possible because arrays are covariant:
        //   Wherever we have an array of Animal,
        //   we can have an array of Cat.
        // Cat <= Animal, so Cat[] <= Animal[]
        Animal[] animals = cats;
        animals[0] = dog; // bad. Is animals[0] a Cat or Dog?
        return cats[0];
    }

    public static void main(String[] args) {
        Dog dog = new Dog();
        Cat cat = dog2cat(dog);
        System.out.println("Hello world!");
    }

}

Java then added ArrayLists and made them invariant instead. 

import java.util.ArrayList;

class Animal {}

class Dog extends Animal {}

class Cat extends Animal {}

public class Dog2Cat2 {
    public static Cat dog2cat(Dog dog) {
        ArrayList<Cat> cats = new ArrayList<>(10);
        // ArrayLists are invariant:
        // Cat <= Animal, but ArrayList<Cat> </= ArrayList<Animal>
        ArrayList<Animal> animals = cats; // no longer allowed
        animals.add(dog);
        return cats.get(0);
    }

    public static void main(String[] args) {
        Dog dog = new Dog();
        Cat cat = dog2cat(dog);
        System.out.println("Hello world!");
    }

}

But despite that, Amin and Tate proceeded to show that Java's (and Scala's) type systems are unsound: https://io.livecode.ch/learn/namin/unsound

2025-12-05 Fri 11:50

Announcements RSS