Books / Applied Functional Programming Tutorial / Chapter 15

GHC Extensions and Dependent Types

In this chapter

GHC Language Extensions
Dependent and Refinement Types
- Agda
- Idris
- LiquidHaskell
Further reading

This lecture is a sort of “gourmet” – the concepts presented here are not used every day nor are common in production, nor are they topics to speak over coffee with mediocre programmers. Rather they represent cutting-edge topics that may potentially write the future of programming. Enjoy ;-)

GHC Language Extensions

Language extensions are used to enable language features in Haskell that may seem useful in certain cases. They can be used to loosen restrictions in the type system or add completely new language constructs to Haskell. As you already know, they can be enabled using the {-# LANGUAGE <ext> #-} pragma or using flags -X<ext>. You should always consider using those extensions over normal Haskell, because it may potentially bring some risks. It is advisable to read some discussions on forums.

TypeFamilies

This extension allows use and definition of indexed type and data families to facilitate type-level programming. Indexed type families, or type families for short, are type constructors that represent sets of types. Set members are denoted by supplying the type family constructor with type parameters, which are called type indices. The difference between vanilla parametrized type constructors and family constructors is much like between parametrically polymorphic functions and (ad-hoc polymorphic) methods of type classes. Parametric polymorphic functions behave the same in all type instances, whereas class methods can change their behaviour in dependence on the class type parameters. Similarly, vanilla type constructors imply the same data representation for all type instances, but family constructors can have varying representation types for varying type indices. (see GHC docs)

{-# LANGUAGE TypeFamilies #-}

-- Declare a list-like data family
data family XList a

-- Declare a list-like instance for Char
data instance XList Char = XCons !Char !(XList Char) | XNil

-- Declare a number-like instance for ()
data instance XList () = XListUnit !Int

class XLength a where
  xlength :: XList a -> Int

instance XLength Char where
  xlength XNil = 0
  xlength (XCons _ r) = 1 + xlength r

instance XLength () where
  xlength (XListUnit _) = 1

GADTs

Generalized algebraic data type are a generalization of the algebraic data types that you are familiar with. Basically, they allow you to explicitly write down the types of the constructors. In this chapter, you’ll learn why this is useful and how to declare your own. GADTs are mainly used to implement domain-specific languages, and so this section will introduce them with a corresponding example.

{-# LANGUAGE GADTs #-}

data Expr a where
    I   :: Int  -> Expr Int
    B   :: Bool -> Expr Bool
    Add :: Expr Int -> Expr Int -> Expr Int
    Mul :: Expr Int -> Expr Int -> Expr Int
    Eq  :: Expr Int -> Expr Int -> Expr Bool
    And :: Expr Bool -> Expr Bool -> Expr Bool

eval :: Expr a -> a
eval (I n) = n  -- return Int
eval (B b) = b  -- returns bool
eval (Add e1 e2) = eval e1 + eval e2 -- return Int
eval (Mul e1 e2) = eval e1 * eval e2 -- return Int
eval (Eq  e1 e2) = eval e1 == eval e2  -- returns bool
eval (And e1 e2) = eval e1 && eval e2  -- returns bool

Complete example: Haskell - GADT

QuasiQuotes

Quasiquoting allows programmers to use custom, domain-specific syntax to construct fragments of their program. Along with Haskell’s existing support for domain specific languages, you are now free to use new syntactic forms for your EDSLs. We’ve already seen it used in Yesod or Debug. Another simple use is with Text.RawString.QQ to allow multiline strings:

{-# LANGUAGE QuasiQuotes #-}
import Text.RawString.QQ

multiline :: String
multiline = [r|<HTML>
<HEAD>
<TITLE>Auto-generated html formated source</TITLE>
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=windows-1252">
</HEAD>
<BODY LINK="800080" BGCOLOR="#ffffff">
<P> </P>
<PRE>|]

You can, of course, write your own DSL or simplify the syntax for yourself. All you have to do is implement your QuasiQuoter (part of Template Haskell). For example, you can create a simple string-string map with semicolon and newlines:

{-# LANGUAGE TemplateHaskell #-}
module MapBuilder (mapBuilder) where

import Language.Haskell.TH
import Language.Haskell.TH.Quote

-- | Map Builder quasiquoter
mapBuilder = QuasiQuoter
    { quoteExp  = mapBuilderParser -- expressions
    , quotePat  = undefined        -- patterns
    , quoteType = undefined        -- types
    , quoteDec  = undefined        -- declarations
    }

-- | Split string to two parts by given char
splitByFirst :: String -> Char -> (String, String)
splitByFirst str sep = splitByFirst' "" str
  where
    splitByFirst' a [] = (a, "")
    splitByFirst' a (x:xs)
       | x == sep  = (a, xs)
       | otherwise = splitByFirst' (a++[x]) xs

-- | Trim spaces and tabs from left of the string
trimLeft :: String -> String
trimLeft "" = ""
trimLeft (x:xs)
  | x `elem` [' ', '\t'] = trimLeft xs
  | otherwise        = x : trimLeft xs

-- | Parse [(String, String)] map from String
mapBuilderParser :: String -> Q Exp
mapBuilderParser = return . ListE . map parseTuples . filter (/="") . map trimLeft . lines
  where
    parseTuples :: String -> Exp
    parseTuples xs = TupE [LitE . StringL $ key, LitE . StringL $ val]
      where
        parts = splitByFirst xs ':'
        key = fst parts
        val = snd parts

Then you can simply import defined quasiquoter and use it:

{-# LANGUAGE QuasiQuotes #-}

import MapBuilder

mymap1 :: [(String, String)]
mymap1 = [mapBuilder|
           a:10
           b:22
           c:hello
           it:has:no:problem
         |]

mymap2 :: [(String, Int)]
mymap2 = map strstr2strint [mapBuilder|
           suchama4:1210
           perglr:1535
         |]

strstr2strint :: (String, String) -> (String, Int)
strstr2strint (x, y) = (x, read y)

Beautiful, right?!

Template Haskell

Template Haskell is a GHC extension to Haskell that adds compile-time metaprogramming facilities. The original design can be found here: http://research.microsoft.com/en-us/um/people/simonpj/papers/meta-haskell/. You could have seen part of it in action in the previous section about quasiquoting but it can do much more although quasiquotes are an important part of it. Great explanation is here and here.

A dependent type is a type whose definition depends on a value. Such types can be for example:

pair of integers where the second is greater than the first,
people with age between 18 and 65,
string in email format (matches given regex).

Dependent types add complexity to a type system. Deciding the equality of dependent types in a program may require computations. If arbitrary values are allowed in dependent types, then deciding type equality may involve deciding whether two arbitrary programs produce the same result; hence type checking may become undecidable.

Agda

Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with the implementation described in his PhD thesis. But current version, Agda 2, is a completely rewritten previous Agda from 1999.

Visit https://github.com/agda/agda where you find some examples as well!

Idris

Idris is a general-purpose purely functional programming language with dependent types, strict or optional lazy evaluation and features such as a totality checker. Idris is highly affected by Haskell and Agda which is visible in its syntax.

Its features are influenced by Haskell and ML, and include:

Full dependent types with dependent pattern matching
Simple foreign function interface (to C)
Compiler-supported interactive editing: the compiler helps you write code using the types where clauses, with a rule, simple case expressions, pattern matching let and lambda bindings
Dependent records with projection and update
Interfaces (similar to type classes in Haskell)
Type-driven overloading resolution
do notation and idiom brackets
Indentation significant syntax
Extensible syntax
Cumulative universes
Totality checking
Hugs-style interactive environment

On their website, you can find a documentation with examples such as Vectors:

infixr 5 ::

data Vect : Nat -> Type -> Type where
    Nil  : Vect Z a
    (::) : a -> Vect k a -> Vect (S k) a

app : Vect n a -> Vect m a -> Vect (n + m) a
app Nil       ys = ys
app (x :: xs) ys = x :: app xs ys

LiquidHaskell

LiquidHaskell is a static verifier for Haskell, based on Liquid Types. It allows annotating code with invariants that complement the invariants imposed by the types. These invariants are checked with a SMT solver. It is not about dependent types but refinement types (you refine some defined type with rules, not build it dependent from the scratch).

Visit: https://ucsd-progsys.github.io/liquidhaskell-blog/

{--! run liquid with no-termination -}

module SimpleRefinements where
import Prelude hiding ((!!), length)
import Language.Haskell.Liquid.Prelude


-- |Simple Refinement Types

{-@ zero :: {v:Int | v = 0} @-}
zero     :: Int
zero     =  0

{-@ type Even = {v:Int | v mod 2 = 0} @-}

{-@ zero'' :: Even @-}
zero''     :: Int
zero''     =  0

-- |Lists

infixr `C`
data L a = N | C a (L a)

{-@ natList :: L Nat @-}
natList     :: L Int
natList     =  0 `C` 1 `C` 3 `C` N

{-@ evenList :: L Even @-}
evenList     :: L Int
evenList     =  0 `C` 2 `C` 8 `C` N

Related Books

Books / Applied Functional Programming Tutorial / Chapter 15

GHC Extensions and Dependent Types

In this chapter

GHC Language Extensions

TypeFamilies

GADTs

QuasiQuotes

Template Haskell

Dependent and Refinement Types

Agda

Idris

LiquidHaskell

Further reading

Licenses and Attributions

Original Content License

Speak Your Mind Cancel reply