TypeSubst.lhs 3.59 KB
Newer Older
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1
2
3
4
5
6
7
8
9
10
11

% $Id: TypeSubst.lhs,v 1.2 2004/02/08 22:14:01 wlux Exp $
%
% Copyright (c) 2003, Wolfgang Lux
% See LICENSE for the full license.
%
\nwfilename{TypeSubst.lhs}
\section{Type Substitutions}
This module implements substitutions on types.
\begin{verbatim}

Björn Peemöller 's avatar
Björn Peemöller committed
12
> module Base.TypeSubst
13
>   ( module Base.TypeSubst, idSubst, singleSubst, bindSubst, compose
Björn Peemöller 's avatar
Björn Peemöller committed
14
>   ) where
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
15

Björn Peemöller 's avatar
Björn Peemöller committed
16
17
> import Data.List (nub)
> import Data.Maybe (fromJust, isJust)
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
18

Björn Peemöller 's avatar
Björn Peemöller committed
19
> import Base.Subst
Björn Peemöller 's avatar
Björn Peemöller committed
20
> import Base.TopEnv
Björn Peemöller 's avatar
Björn Peemöller committed
21
22
> import Base.Types

Björn Peemöller 's avatar
Björn Peemöller committed
23
> import Env.Value (ValueInfo (..))
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

> type TypeSubst = Subst Int Type

> class SubstType a where
>   subst :: TypeSubst -> a -> a

> bindVar :: Int -> Type -> TypeSubst -> TypeSubst
> bindVar tv ty = compose (bindSubst tv ty idSubst)

> substVar :: TypeSubst -> Int -> Type
> substVar = substVar' TypeVariable subst

> instance SubstType Type where
>   subst sigma (TypeConstructor tc tys) =
>     TypeConstructor tc (map (subst sigma) tys)
39
40
41
42
43
>   subst sigma (TypeVariable        tv) = substVar sigma tv
>   subst sigma (TypeConstrained tys tv) = case substVar sigma tv of
>     TypeVariable tv' -> TypeConstrained tys tv'
>     ty -> ty
>   subst sigma (TypeArrow      ty1 ty2) =
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
44
>     TypeArrow (subst sigma ty1) (subst sigma ty2)
45
46
47
>   subst _     ts@(TypeSkolem        _) = ts
>   subst sigma (TypeRecord       fs rv)
>     | isJust rv = case substVar sigma (fromJust rv) of
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
48
>         TypeVariable tv -> TypeRecord fs' (Just tv)
49
>         ty              -> ty
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
50
51
52
53
54
55
56
57
58
59
60
61
>     | otherwise = TypeRecord fs' Nothing
>    where fs' = map (\ (l,ty) -> (l, subst sigma ty)) fs

> instance SubstType TypeScheme where
>   subst sigma (ForAll n ty) =
>     ForAll n (subst (foldr unbindSubst sigma [0..n-1]) ty)

> instance SubstType ExistTypeScheme where
>   subst sigma (ForAllExist n n' ty) =
>     ForAllExist n n' (subst (foldr unbindSubst sigma [0..n+n'-1]) ty)

> instance SubstType ValueInfo where
62
63
64
65
>   subst _     dc@(DataConstructor  _ _ _) = dc
>   subst _     nc@(NewtypeConstructor _ _) = nc
>   subst theta (Value              v a ty) = Value v a (subst theta ty)
>   subst theta (Label              l r ty) = Label l r (subst theta ty)
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83

> instance SubstType a => SubstType (TopEnv a) where
>   subst = fmap . subst

\end{verbatim}
The function \texttt{expandAliasType} expands all occurrences of a
type synonym in a type. After the expansion we have to reassign the
type indices for all type variables. Otherwise, expanding a type
synonym like \verb|type Pair' a b = (b,a)| could break the invariant
that the universally quantified type variables are assigned indices in
the order of their occurrence. This is handled by the function
\texttt{normalize}.
\begin{verbatim}

> expandAliasType :: [Type] -> Type -> Type
> expandAliasType tys (TypeConstructor tc tys') =
>   TypeConstructor tc (map (expandAliasType tys) tys')
> expandAliasType tys (TypeVariable n)
Björn Peemöller 's avatar
Björn Peemöller committed
84
>   | n >= 0    = tys !! n
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
85
>   | otherwise = TypeVariable n
Björn Peemöller 's avatar
Björn Peemöller committed
86
87
> expandAliasType _   (TypeConstrained   tys n) = TypeConstrained tys n
> expandAliasType tys (TypeArrow       ty1 ty2) =
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
88
>   TypeArrow (expandAliasType tys ty1) (expandAliasType tys ty2)
Björn Peemöller 's avatar
Björn Peemöller committed
89
90
> expandAliasType _   tsk@(TypeSkolem        _) = tsk
> expandAliasType tys (TypeRecord        fs rv)
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
91
>   | isJust rv =
Björn Peemöller 's avatar
Björn Peemöller committed
92
>     let (TypeVariable tv) = expandAliasType tys $ TypeVariable $ fromJust rv
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
93
94
95
>     in  TypeRecord fs' (Just tv)
>   | otherwise =
>     TypeRecord fs' Nothing
Björn Peemöller 's avatar
Björn Peemöller committed
96
>  where fs' = map (\ (l, ty) -> (l, expandAliasType tys ty)) fs
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
97
98

> normalize :: Type -> Type
Björn Peemöller 's avatar
Björn Peemöller committed
99
100
> normalize ty = expandAliasType [TypeVariable (occur tv) | tv <- [0 ..]] ty
>   where tvs = zip (nub (filter (>= 0) (typeVars ty))) [0 ..]
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
101
102
103
>         occur tv = fromJust (lookup tv tvs)

\end{verbatim}