Avoid overlapping instances with closed type families

- February 5, 2017
Kwang's Haskell Blog - Avoid overlapping instances with closed type families

Avoid overlapping instances with closed type families

Posted on February 5, 2017 by Kwang Yul Seo

Overlapping instances are one of the most controversial features in Haskell. Fortunately, there are many tricks that let us avoid overlapping instances. In this post, I will introduce one such trick which uses closed type families.

Why overlapping instances are bad

In Haskell, we expect adding an extra instance in one module does not cause any other modules that depend on the given module to fail to compile or have different behaviors as long as the dependent modules use explicit import lists.

Unfortunately, OverlappingInstances breaks this expectation.

  • Module A
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}

module A where

class C a b c | a b -> c where
  f :: a -> b -> c

instance C String a String where
  f s _ = s
  • Module B
module B where

import A(C(..))

func :: String -> Int -> String
func = f

func "foo" 3 evaluates to "foo".

Let’s add a new instance declaration in A.

instance {-# OVERLAPPING #-} C String Int String where
  f s i = concat $ replicate i s

Module B still compiles, but func "foo" 3 now evaluates to "foofoofoo" because C String Int String is more specific than C String a String.

Wen can see that adding an extra instance silently broke the backward compatibility. To make the matters worse, there is no way to go back to the old behavior. GHC automatically chooses a more specific instance. In this case, C String Int String is chosen because it is more specific than C String a String.

Use cases of overlapping instances

Overlapping instances are controversial because they are too useful to remove. Overlapping instances are appealing because they express the common pattern of adding a special case to an existing set of overloaded functions.

Let’s check how show method from Prelude handles a list.

λ> show [1,2,3]
"[1,2,3]"
λ> show [False, True, False]
"[False,True,False]"

It converts a given list to a string by putting a comma between elements. According to the rule, it must show "foo" as ['f', 'o', 'o']. But show handles a string (a list of characters) in a different manner.

λ> show "abc"
"\"abc\""

This requires overlapping instances because [a] overlaps with [Char].

instance Show a => Show [a] where
  ...

instance {-# OVERLAPPING #-} Show [Char] where
  ...

Haskell 98 solution

Haskell Prelude avoided overlapping instances by using the extra-method trick. The trick does not require any GHC extensions, but class definitions become more complicated. Interested readers are referred to Brandon Simmons’s How the Haskell Prelude Avoids Overlapping Instances in Show for the details.

Another solution with closed type families

This solution is a variation of the solution introduced in Overcoming Overlapping section of Oleg Kiselyov’s Type equality predicates: from OverlappingInstances to overcoming them.

Here’s the list of GHC extensions and imports we need.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Proxy

F is a type-level function which returns 'True for Char and 'False for any other types. This does not require overlapping instances because the set of special cases are closed.

type family (F a) :: Bool where
  F Char  = 'True
  F a     = 'False

ShowList class defines showl method.

class ShowList a where
  showl :: [a] -> String

The type checker computes the type of flag by evaluating F a and dispatches the method based on the type of flag. If it is 'True, it searches the special case instances. Otherwise, it searches the generic case instance.

instance (F a ~ flag, ShowList' flag a) => ShowList a where
  showl = showl' (Proxy :: Proxy flag)

class ShowList' (flag :: Bool) a where
  showl' :: Proxy flag -> [a] -> String

instance ShowList' 'True Char where
  showl' _ x = x

instance (Show a) => ShowList' 'False a where
  showl' _ x = show x

We can add another special case for Bool as follows:

type family (F a) :: Bool where
  F Char  = 'True
  F Bool  = 'True
  F a     = 'False

instance ShowList' 'True Bool where
  showl' _ x = map toBinaryDigit x
    where toBinaryDigit False = '0'
          toBinaryDigit True  = '1'

Now showList [True,False,True] evaluates to 101 instead of [True,False,True].

Other solutions

Oleg Grenrus’s gist contains other workarounds for OverlappingInstances.

Read more

Type-level insertion sort

- January 30, 2017
Kwang's Haskell Blog - Type-level insertion sort

Type-level insertion sort

Posted on January 30, 2017 by Kwang Yul Seo

Multi-parameter type classes and functional dependencies made type-level programming possible. Back in 2000, Thomas Hallgren showed an implementation of insertion sort as an example of static computation using functional dependencies. The code has a strong resemblance to logic programming which looks bizarre to most functional programmers. In this post, I will show you a more “functional-style” implementation of insertion sort using closed type families.

Term-level insertion sort

Here’s an implementation of insertion sort we all know.

sort :: (Ord a) => [a] -> [a]
sort [] = []
sort (x : xs) = insert x (sort xs)

insert :: (Ord a) => a -> [a] -> [a]
insert x [] = x : []
insert x (y : ys) = insert' (compare x y) x y ys

insert' :: (Ord a) => Ordering -> a -> a -> [a] -> [a]
insert' LT  x y ys = x : (y : ys)
insert' _   x y ys = y : insert x ys

l = [1, 3, 2, 4, 7, 9, 5]

sort l sorts the given list.

λ> sort l
[1,2,3,4,5,7,9]

To implement insertion sort in type-level, we must be able to define

  1. naturals, booleans and lists
  2. functions

in type-level. For the basics of type-level programming, readers are referred to Type-level functions using closed type families.

Insertion sort

Here’s an implementation of type-level insertion sort. One can see the strong similarity with the term-level insertion sort.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

type family Sort xs where
  Sort '[] = '[]
  Sort (x ': xs) = Insert x (Sort xs)

type family Insert x xs where
  Insert x '[] = x ': '[]
  Insert x (y ': ys) = Insert' (CmpNat x y) x y ys

type family Insert' b x y ys where
  Insert' 'LT  x y ys = x ': (y ': ys)
  Insert' _    x y ys = y ': Insert x ys

type L = [1, 3, 2, 4, 7, 9, 5]

In this simple scenario, converting a term-level function into a type-level function is almost mechanical. Just a few rules suffice.

  • sort -> type family Sort
  • [] -> ’[]
  • (x : xs) -> (x ’: xs)
  • compare -> CmpNat

We can evaluate Sort L using GHCi’s kind! command.

λ> :kind! Sort L
Sort L :: [Nat]
= '[1, 2, 3, 4, 5, 7, 9]
Read more

Type-level functions using closed type families

- January 16, 2017
Kwang's Haskell Blog - Type-level functions using closed type families

Type-level functions using closed type families

Posted on January 16, 2017 by Kwang Yul Seo

In this post, we will see how to write basic type-level functions using closed type families.

Before we start, let’s declare a bunch of GHC language extensions required to use type-level functions.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

Also import required modules. GHC.TypeLits provides type-level natural numbers and symbols.

import GHC.TypeLits
import Data.Proxy

Literals

Datatype promotion allows us to use True and False as type constructors whose kind is Bool. The quotes are used to emphasize the promotion, but can be omitted when syntactically unambiguous.

λ> :set -XDataKinds
λ> :kind 'True
'True :: Bool
λ> :kind 'False
'False :: Bool

We can also use numbers such as 1 and 2 as types. The kind of these numbers is Nat.

λ> :kind 1
1 :: Nat

Type-level Function

If takes three arguments c, t and e and returns t if c is True, returns e otherwise. The kind of If is Bool -> * -> * -> *.

type family If c t e where
  If 'True  t e = t
  If 'False t e = e

We can use GHCi’s kind! command to evaluate type functions.

λ> :kind! If 'True Bool Char
If 'True Bool Char :: *
= Bool
λ> :kind! If 'False Int Double
If 'False Int Double :: *
= Double

Type-level List

As we can promote types like Bool, we can also promote lists and treat [] as a kind constructor, and [] and (:) as types.

When (:) is seen as a type constructor, it has kind

λ> :kind (:)
(:) :: a -> [a] -> [a]

It means (:) is kind-polymorphic.

So we can create a type-level list of booleans as well as naturals.

λ> :kind [True, False]
[True, False] :: [Bool]
λ> :kind [1, 2]
[1,2] :: [Nat]

Type-level List Function

The definition of type-level function Length is the same as the value level length function. If it an empty list returns 0. If it not empty, add 1 to the length of the tail.

type family Length xs where
   Length '[]       = 0
   Length (x ': xs) = 1 + Length xs

0 and 1 are types of Nat kind and (+) is a type-level add function defined in GHC.TypeLits. We can even use (:) as a pattern here.

λ> :kind! Length [Char,Bool,Int]
Length [Char,Bool,Int] :: Nat
= 3

It seems Length is almost identical to the value level function length, but Length function is not kind-polymorphic by default. Thus passing [1, 2, 3] to Length causes an error.

λ> :kind! Length [1,2,3]

<interactive>:1:8: error:
    • Expected kind ‘[*]’, but ‘'[1, 2, 3]’ has kind ‘[Nat]’
    • In the first argument of ‘Length’, namely ‘'[1, 2, 3]’
      In the type ‘Length '[1, 2, 3]’

To make it poly-kinded, we need to turn on PolyKind extension. The kind is inferred automatically, but we can also specify the kind with k.

type family Length (xs :: [k]) where
   Length '[]       = 0
   Length (x ': xs) = 1 + Length xs

Head and Tail are defined in a similar manner. Note that the kind of xs is explicitly annotated with [*] because they only work on type-level lists.

type family Head (xs :: [*]) where
   Head (x ': xs) = x

type family Tail (xs :: [*]) where
  Tail (x ': xs) = xs

We can see Head and Tail work as expected.

λ> :kind! Head [Char, Bool, Int]
Head [Char, Bool, Int] :: *
= Char
*Main
λ> :kind! Tail [Char, Bool, Int]
Tail [Char, Bool, Int] :: [*]
= '[Bool, Int]

One notable thing here is that both Head and Tail are partially defined. What if we pass '[] to Head or Tail?

λ> :kind! Head '[]
Head '[] :: GHC.Types.*
= Head '[]

It seems GHC treats Head '[] as a valid type instead of emitting a type error. It is a bit mysterious, but at least we can see that type-level functions in Haskell can be partial and the behavior is not intuitive. Interested readers are referred to Richard Eisenberg’s What are type families? which discusses this issue in details.

Higher-order Type-level List Function

It is even possible to define type-level map function. Map takes a type-level function f and a type-level list xs. It applies f to every element of xs and returns a new type-level list containing the results.

type family Map (f :: * -> *) (xs :: [*]) where
   Map f '[]       = '[]
   Map f (x ': xs) = f x ': Map f xs
λ> :kind! Map MakePair [Char,Bool,Int]
Map MakePair [Char,Bool,Int] :: [GHC.Types.*]
= '[(Char, Char), (Bool, Bool), (Int, Int)]

where the definition of MakePair is

type family MakePair (x :: *) where
  MakePair x = (x, x)

Wrap-up

So far we’ve covered only the basics of type-level datatypes and functions. Recent additions to GHC make it possible to explore the whole new world of dependent type programming in Haskell. Interested readers might want to take a look at the publications of Richard A. Eisenberg whose current work is to add dependent types to Haskell.

Read more