AN OVERVIEW OF THE�

​

​

TYPE SYSTEM

Intro

“PureScript is a small strongly-typed programming language that compiles to JavaScript”

• Learn more at purescript.org or on #purescript
• Goals:
• Build the language I want to use every day
• Explore how types can improve web programming
• Try out some new type system ideas
• Provide a fun project for Haskell OSS newcomers

Agenda

• Recap some Haskell extensions
• Talk about the implementation
• Demo some novel features
• Future work

Some Haskell Extensions

Type Classes

class Eq a where� eq :: a -> a -> Boolean��instance eqBoolean :: Eq Boolean where� eq True True = True� eq False False = True� eq _ _ = False��instance eqList :: Eq a => Eq (List a) where� ...

Higher-kinded types

data Free f a� = Pure a� | Impure (f (Free f a))

​

class Functor f where� map :: (a -> b) -> f a -> f b

Functional Dependencies

class MonadState s m | m -> s where� state :: (s -> Tuple s a) -> m a

​

data Z�data S n -- Peano naturals��class Add n m r | n m -> r�instance addZ :: Add Z n n�instance addS :: Add n m r => Add (S n) m (S r)�

Functional Dependencies

Functional dependencies give us “type-level Prolog”

Examples:

• purescript-generics-rep
• purescript-type-map by @LiamGoodacre
• purescript-type-lang by @LiamGoodacre

Higher-rank polymorphism

runST :: forall a. (forall h. ST h a) -> a

�hiding� :: forall result� . (forall impl. Interface impl => Proxy impl -> result)� -> result�

Implementation Notes

Phases of the type checker

1. Check/infer types and gather constraints
2. Solve constraints
3. goto 2 until no more constraints can be solved
4. Final cleanup pass and generalization

​

Unification

Types can be partially solved during type checking

Unification happens when we learn that two (partially known) types must be equal

​

​

​

(Example)

Bidirectional type checking

Separate the type checker into two modes: inference and checking

​

In practice, there are several judgments:

• Inference
• Checking
• Function application
• Subsumption

Skolemization

When checking something has a polymorphic type, we need to generate a fresh type variable which does not unify with other types.

These are called skolem constants.

At the end of type checking, we need to check that no skolem constants escaped their scope.

​

(Example)

Type Classes

When we apply a function which has type class constraints, we insert a placeholder for a dictionary into the expression.

This is called elaboration or dictionary-passing.

These placeholders will get replaced during the solving phase.

​

​

(Example)

Functional Dependencies

Functional dependencies can cause new unifications to happen during solving.

These unifications can cause more instances to become applicable, solving new constraints.

So the solver loops until no new type information can be learned.

​

​

(Example)

Cleanup

• Check no skolems escaped
• Generalize any unsolved type variables
• Generalize over any unsolved constraints

Novel Features

Row Polymorphism: Extensible Records

getter :: forall a r� . { foo :: a | r }� -> a �getter rec = rec.foo

setter :: forall a r� . a� -> { foo :: a | r }� -> { foo :: a | r } �setter a rec = rec { foo = a }

Row Polymorphism: Extensible Effects

getFromNetwork� :: forall eff� . Eff (network :: NETWORK | eff) X��main :: Eff (console :: CONSOLE, network :: NETWORK) Unit�main = do� x <- getNetworkResource� logShow x

Row Polymorphism: Implementation

• Rows are maps from labels to types�(actually, association lists)
• Rows can have duplicate labels
• Unification of rows must ignore order of different labels but preserve order of duplicates
• “row of k”, spelled # k is a new kind for each kind k

​

​

(Example)

Row Constraints: Unions

-- a magic type class�class Union r1 r2 r3 | r1 r2 -> r3, r1 r3 -> r2��merge :: forall r1 r2 r3.� . Union r1 r2 r3� => Record r1� -> Record r2� -> Record r3�

See purescript-records by @doolse, also Ermine

Polymorphic Labels

-- another magic type class�class RowCons l a r1 r2 | l a r1 -> r2, l r1 r2 -> a��prop :: forall l a r1 r2.� . RowCons l a r1 r2� => SProxy l� -> Lens’ (Record r2) a

​

See purescript-profunctor-lenses

Polymorphic Labels: Variants

ctor :: forall l a r1 r2.� . RowCons l a r1 r2� => SProxy l� -> Prism’ (Variant r2) a

​

​

​

See purescript-variants by @natefaubion

Type-Directed Search

flatten :: List (Maybe Int) -> Maybe (List Int)�flatten = ?IForgot

���Hole 'IForgot' has the inferred type�� List (Maybe Int) -> Maybe (List Int)��You could substitute the hole with one of these values:�� Data.Monoid.mempty :: forall m. Monoid m => m� Data.Traversable.sequence :: forall a m t. Traversable t => Applicative m => t (m a) -> m (t a)

​

​

​

​

Type-Directed Search: Implementation

• Brute-force search through the context
• Uses subsumption to test for compatibility������

​

See @kritzcreek’s thesis :)

Future Work

Instance Chains

class TypeEq a b r | a b -> r��instance typeEq :: TypeEq a a True�instance typeNotEq :: TypeEq a b False -- ← overlapping!

​

instances� instance typeEq :: TypeEq a a True� instance typeNotEq :: TypeEq a b False

​

Constraint Kinds

class MapRow (c :: Symbol -> Type -> Type -> Constraint)� (r1 :: # Type)� (r2 :: # Type)��-- auto-generated instances�instance mapEmpty :: MapRow c () ()�instance mapNonEmpty � :: (c l a b, MapRow xs ys) =>� MapRow (l :: a | xs) (l :: a | ys)

​

References

Haskell 98

• Typing Haskell in Haskell�Mark P. Jones

​

Higher-rank Polymorphism

• Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism�Joshua Dunfield and Neelakantan R. Krishnaswami
• HMF: Simple Type Inference for First-Class Polymorphism�Daan Leijen

​

Type Classes and Functional Dependencies

• How to make ad-hoc polymorphism less ad hoc�Philip Wadler
• Type Classes with Functional Dependencies�Mark P. Jones
• Instance Chains: Type Class Programming Without Overlapping Instances�J. Garrett Morris and Mark P. Jones

Extensible Records

• Row Polymorphism Isn’t Subtyping�Brian McKenna
• Extensible records with scoped labels�Daan Leijen
• First-class labels for extensible rows�Daan Leijen
• Koka: Programming with Row Polymorphic Effect Types�Daan Leijen
• Ermine compiler

Questions?