{- |
Module : $Header$
Description : Internal representation of types
Copyright : (c) 2002 - 2004 Wolfgang Lux
Martin Engelke
2015 Jan Tikovsky
2016 Finn Teegen
License : BSD-3-clause
Maintainer : bjp@informatik.uni-kiel.de
Stability : experimental
Portability : portable
This module modules provides the definitions for the internal
representation of types in the compiler along with some helper functions.
-}
-- TODO: Use MultiParamTypeClasses ?
module Base.Types
( -- * Representation of types
Type (..), applyType, unapplyType, rootOfType
, isArrowType, arrowArity, arrowArgs, arrowBase, arrowUnapply
, IsType (..), typeConstrs
, qualifyType, unqualifyType, qualifyTC
-- * Representation of predicate, predicate sets and predicated types
, Pred (..), qualifyPred, unqualifyPred
, PredSet, emptyPredSet, partitionPredSet, minPredSet, maxPredSet
, qualifyPredSet, unqualifyPredSet
, PredType (..), predType, unpredType, qualifyPredType, unqualifyPredType
-- * Representation of data constructors
, DataConstr (..), constrIdent, constrTypes, recLabels, recLabelTypes
, tupleData
-- * Representation of class methods
, ClassMethod (..), methodName, methodArity, methodType
-- * Representation of quantification
, TypeScheme (..), monoType, polyType, typeScheme
, rawType
-- * Predefined types
, arrowType, unitType, predUnitType, boolType, predBoolType, charType
, intType, predIntType, floatType, predFloatType, stringType, predStringType
, listType, consType, ioType, tupleType
, numTypes, fractionalTypes
, predefTypes
) where
import qualified Data.Set.Extra as Set
import Curry.Base.Ident
import Base.Messages (internalError)
import Env.Class (ClassEnv, allSuperClasses)
-- ---------------------------------------------------------------------------
-- Types
-- ---------------------------------------------------------------------------
-- A type is either a type constructor, a type variable, an application
-- of a type to another type, or an arrow type. Although the latter could
-- be expressed by using 'TypeApply' with the function type constructor,
-- we currently use 'TypeArrow' because arrow types are used so frequently.
-- The 'TypeConstrained' case is used for representing type variables that
-- are restricted to a particular set of types. At present, this is used
-- for typing integer literals, which are restricted to types 'Int' and
-- 'Float'. If the type is not restricted, it defaults to the first type
-- from the constraint list.
-- Type variables are represented with deBruijn style indices. Universally
-- quantified type variables are assigned indices in the order of their
-- occurrence in the type from left to right. This leads to a canonical
-- representation of types where alpha-equivalence of two types
-- coincides with equality of the representation.
-- Note that even though 'TypeConstrained' variables use indices
-- as well, these variables must never be quantified.
-- Note further that the order of constructors is important for the derived
-- 'Ord' instance. In particular, it is essential that the type variable
-- is considered less than the type application (see predicates and predicate
-- sets below for more information).
data Type
= TypeConstructor QualIdent
| TypeVariable Int
| TypeConstrained [Type] Int
| TypeApply Type Type
| TypeArrow Type Type
| TypeForall [Int] Type
deriving (Eq, Ord, Show)
-- The function 'applyType' applies a type to a list of argument types,
-- whereas applications of the function type constructor to two arguments
-- are converted into an arrow type. The function 'unapplyType' decomposes
-- a type into a root type and a list of argument types.
applyType :: Type -> [Type] -> Type
applyType (TypeConstructor tc) tys
| tc == qArrowId && length tys == 2 = TypeArrow (tys !! 0) (tys !! 1)
applyType (TypeApply (TypeConstructor tc) ty) tys
| tc == qArrowId && length tys == 1 = TypeArrow ty (head tys)
applyType ty tys = foldl TypeApply ty tys
unapplyType :: Bool -> Type -> (Type, [Type])
unapplyType dflt ty = unapply ty []
where
unapply (TypeConstructor tc) tys = (TypeConstructor tc, tys)
unapply (TypeApply ty1 ty2) tys = unapply ty1 (ty2 : tys)
unapply (TypeVariable tv) tys = (TypeVariable tv, tys)
unapply (TypeArrow ty1 ty2) tys =
(TypeConstructor qArrowId, ty1 : ty2 : tys)
unapply (TypeConstrained tys tv) tys'
| dflt = unapply (head tys) tys'
| otherwise = (TypeConstrained tys tv, tys')
unapply (TypeForall tvs ty') tys = (TypeForall tvs ty', tys)
-- The function 'rootOfType' returns the name of the type constructor at the
-- root of a type. This function must not be applied to a type whose root is
-- a type variable or a skolem type.
rootOfType :: Type -> QualIdent
rootOfType ty = case fst (unapplyType True ty) of
TypeConstructor tc -> tc
_ -> internalError $ "Base.Types.rootOfType: " ++ show ty
-- The function 'isArrowType' checks whether a type is a function
-- type t_1 -> t_2 -> ... -> t_n. The function 'arrowArity' computes
-- the arity n of a function type, 'arrowArgs' computes the types
-- t_1 ... t_n-1 and 'arrowBase' returns the type t_n. 'arrowUnapply'
-- combines 'arrowArgs' and 'arrowBase' in one call.
isArrowType :: Type -> Bool
isArrowType (TypeArrow _ _) = True
isArrowType _ = False
arrowArity :: Type -> Int
arrowArity = length. arrowArgs
arrowArgs :: Type -> [Type]
arrowArgs = fst . arrowUnapply
arrowBase :: Type -> Type
arrowBase = snd. arrowUnapply
arrowUnapply :: Type -> ([Type], Type)
arrowUnapply (TypeArrow ty1 ty2) = (ty1 : tys, ty)
where (tys, ty) = arrowUnapply ty2
arrowUnapply ty = ([], ty)
-- The function 'typeConstrs' returns a list of all type constructors
-- occuring in a type t.
typeConstrs :: Type -> [QualIdent]
typeConstrs ty = constrs ty [] where
constrs (TypeConstructor tc) tcs = tc : tcs
constrs (TypeApply ty1 ty2) tcs = constrs ty1 (constrs ty2 tcs)
constrs (TypeVariable _) tcs = tcs
constrs (TypeConstrained _ _) tcs = tcs
constrs (TypeArrow ty1 ty2) tcs = constrs ty1 (constrs ty2 tcs)
constrs (TypeForall _ ty') tcs = constrs ty' tcs
-- The method 'typeVars' returns a list of all type variables occurring in a
-- type t. Note that 'TypeConstrained' variables are not included in the set of
-- type variables because they cannot be generalized.
class IsType t where
typeVars :: t -> [Int]
instance IsType Type where
typeVars = typeVars'
typeVars' :: Type -> [Int]
typeVars' ty = vars ty [] where
vars (TypeConstructor _) tvs = tvs
vars (TypeApply ty1 ty2) tvs = vars ty1 (vars ty2 tvs)
vars (TypeVariable tv) tvs = tv : tvs
vars (TypeConstrained _ _) tvs = tvs
vars (TypeArrow ty1 ty2) tvs = vars ty1 (vars ty2 tvs)
vars (TypeForall tvs' ty') tvs = filter (`notElem` tvs') (typeVars' ty') ++ tvs
-- The functions 'qualifyType' and 'unqualifyType' add/remove the
-- qualification with a module identifier for type constructors.
qualifyType :: ModuleIdent -> Type -> Type
qualifyType m (TypeConstructor tc) = TypeConstructor (qualifyTC m tc)
qualifyType m (TypeApply ty1 ty2) =
TypeApply (qualifyType m ty1) (qualifyType m ty2)
qualifyType _ tv@(TypeVariable _) = tv
qualifyType m (TypeConstrained tys tv) =
TypeConstrained (map (qualifyType m) tys) tv
qualifyType m (TypeArrow ty1 ty2) =
TypeArrow (qualifyType m ty1) (qualifyType m ty2)
qualifyType m (TypeForall tvs ty) = TypeForall tvs (qualifyType m ty)
unqualifyType :: ModuleIdent -> Type -> Type
unqualifyType m (TypeConstructor tc) = TypeConstructor (qualUnqualify m tc)
unqualifyType m (TypeApply ty1 ty2) =
TypeApply (unqualifyType m ty1) (unqualifyType m ty2)
unqualifyType _ tv@(TypeVariable _) = tv
unqualifyType m (TypeConstrained tys tv) =
TypeConstrained (map (unqualifyType m) tys) tv
unqualifyType m (TypeArrow ty1 ty2) =
TypeArrow (unqualifyType m ty1) (unqualifyType m ty2)
unqualifyType m (TypeForall tvs ty) = TypeForall tvs (unqualifyType m ty)
qualifyTC :: ModuleIdent -> QualIdent -> QualIdent
qualifyTC m tc | isPrimTypeId tc = tc
| otherwise = qualQualify m tc
-- ---------------------------------------------------------------------------
-- Predicates
-- ---------------------------------------------------------------------------
data Pred = Pred QualIdent Type
deriving (Eq, Show)
-- We provide a custom 'Ord' instance for predicates here where we consider
-- the type component of the predicate before the class component. This way,
-- we ensure that a class method's implicit class constraint is always the
-- minimum w.r.t. this order, because the type expression for that constraint
-- is a type variable with index 0 and there are no other class constraints
-- in a predicate set that constraint the same type variable as restrictions
-- on class variables are not allowed (see predicate sets below for more
-- information why this order is relevant).
instance Ord Pred where
Pred qcls1 ty1 `compare` Pred qcls2 ty2 = case ty1 `compare` ty2 of
LT -> LT
EQ -> qcls1 `compare` qcls2
GT -> GT
instance IsType Pred where
typeVars (Pred _ ty) = typeVars ty
qualifyPred :: ModuleIdent -> Pred -> Pred
qualifyPred m (Pred qcls ty) = Pred (qualQualify m qcls) (qualifyType m ty)
unqualifyPred :: ModuleIdent -> Pred -> Pred
unqualifyPred m (Pred qcls ty) =
Pred (qualUnqualify m qcls) (unqualifyType m ty)
-- ---------------------------------------------------------------------------
-- Predicate sets
-- ---------------------------------------------------------------------------
-- A predicate set is an ordered set of predicates. This way, we do not
-- have to manually take care of duplicate predicates and have automatically
-- achieved a canonical representation (as only original names for type classes
-- are used). Having the order on types and predicates in mind, we have also
-- ensured that a class method's implicit class constraint is always the minimum
-- element of a method's predicate set, thus making it very easy to remove it.
type PredSet = Set.Set Pred
instance (IsType a, Ord a) => IsType (Set.Set a) where
typeVars = concat . Set.toList . Set.map typeVars
emptyPredSet :: PredSet
emptyPredSet = Set.empty
partitionPredSet :: PredSet -> (PredSet, PredSet)
partitionPredSet = Set.partition $ \(Pred _ ty) -> isTypeVariable ty
where
isTypeVariable (TypeVariable _) = True
isTypeVariable (TypeApply ty _) = isTypeVariable ty
isTypeVariable _ = False
-- The function 'minPredSet' transforms a predicate set by removing all
-- predicates from the predicate set which are implied by other predicates
-- according to the super class hierarchy. Inversely, the function 'maxPredSet'
-- adds all predicates to a predicate set which are implied by the predicates
-- in the given predicate set.
minPredSet :: ClassEnv -> PredSet -> PredSet
minPredSet clsEnv ps =
ps `Set.difference` Set.concatMap implied ps
where implied (Pred cls ty) = Set.fromList
[Pred cls' ty | cls' <- tail (allSuperClasses cls clsEnv)]
maxPredSet :: ClassEnv -> PredSet -> PredSet
maxPredSet clsEnv ps = Set.concatMap implied ps
where implied (Pred cls ty) = Set.fromList
[Pred cls' ty | cls' <- allSuperClasses cls clsEnv]
qualifyPredSet :: ModuleIdent -> PredSet -> PredSet
qualifyPredSet m = Set.map (qualifyPred m)
unqualifyPredSet :: ModuleIdent -> PredSet -> PredSet
unqualifyPredSet m = Set.map (unqualifyPred m)
-- ---------------------------------------------------------------------------
-- Predicated types
-- ---------------------------------------------------------------------------
data PredType = PredType PredSet Type
deriving (Eq, Show)
-- When enumarating the type variables and skolems of a predicated type, we
-- consider the type variables occuring in the predicate set after the ones
-- occuring in the type itself.
instance IsType PredType where
typeVars (PredType ps ty) = typeVars ty ++ typeVars ps
predType :: Type -> PredType
predType = PredType emptyPredSet
unpredType :: PredType -> Type
unpredType (PredType _ ty) = ty
qualifyPredType :: ModuleIdent -> PredType -> PredType
qualifyPredType m (PredType ps ty) =
PredType (qualifyPredSet m ps) (qualifyType m ty)
unqualifyPredType :: ModuleIdent -> PredType -> PredType
unqualifyPredType m (PredType ps ty) =
PredType (unqualifyPredSet m ps) (unqualifyType m ty)
-- ---------------------------------------------------------------------------
-- Data constructors
-- ---------------------------------------------------------------------------
-- The type 'DataConstr' is used to represent value or record constructors
-- introduced by data or newtype declarations.
data DataConstr = DataConstr Ident [Type]
| RecordConstr Ident [Ident] [Type]
deriving (Eq, Show)
constrIdent :: DataConstr -> Ident
constrIdent (DataConstr c _) = c
constrIdent (RecordConstr c _ _) = c
constrTypes :: DataConstr -> [Type]
constrTypes (DataConstr _ tys) = tys
constrTypes (RecordConstr _ _ tys) = tys
recLabels :: DataConstr -> [Ident]
recLabels (DataConstr _ _) = []
recLabels (RecordConstr _ ls _) = ls
recLabelTypes :: DataConstr -> [Type]
recLabelTypes (DataConstr _ _) = []
recLabelTypes (RecordConstr _ _ tys) = tys
tupleData :: [DataConstr]
tupleData = [DataConstr (tupleId n) (take n tvs) | n <- [2 ..]]
where tvs = map TypeVariable [0 ..]
-- ---------------------------------------------------------------------------
-- Class methods
-- ---------------------------------------------------------------------------
-- The type 'ClassMethod' is used to represent class methods introduced
-- by class declarations. The 'Maybe Int' denotes the arity of the provided
-- default implementation.
data ClassMethod = ClassMethod Ident (Maybe Int) PredType
deriving (Eq, Show)
methodName :: ClassMethod -> Ident
methodName (ClassMethod f _ _) = f
methodArity :: ClassMethod -> Maybe Int
methodArity (ClassMethod _ a _) = a
methodType :: ClassMethod -> PredType
methodType (ClassMethod _ _ pty) = pty
-- ---------------------------------------------------------------------------
-- Quantification
-- ---------------------------------------------------------------------------
-- We support only universally quantified type schemes
-- (forall alpha . tau(alpha)). Quantified type variables are assigned
-- ascending indices starting from 0. Therefore it is sufficient to record the
-- numbers of quantified type variables in the 'ForAll' constructor.
data TypeScheme = ForAll Int PredType deriving (Eq, Show)
instance IsType TypeScheme where
typeVars (ForAll _ pty) = [tv | tv <- typeVars pty, tv < 0]
-- The functions 'monoType' and 'polyType' translate a type tau into a
-- monomorphic type scheme and a polymorphic type scheme, respectively.
-- 'polyType' assumes that all universally quantified variables in the type are
-- assigned indices starting with 0 and does not renumber the variables.
monoType :: Type -> TypeScheme
monoType = ForAll 0 . predType
polyType :: Type -> TypeScheme
polyType = typeScheme . predType
typeScheme :: PredType -> TypeScheme
typeScheme pty = ForAll (maximum (-1 : typeVars pty) + 1) pty
-- The function 'rawType' strips the quantifier and predicate set from a
-- type scheme.
rawType :: TypeScheme -> Type
rawType (ForAll _ (PredType _ ty)) = ty
-- ---------------------------------------------------------------------------
-- Predefined types
-- ---------------------------------------------------------------------------
primType :: QualIdent -> [Type] -> Type
primType = applyType . TypeConstructor
arrowType :: Type -> Type -> Type
arrowType ty1 ty2 = primType qArrowId [ty1, ty2]
unitType :: Type
unitType = primType qUnitId []
predUnitType :: PredType
predUnitType = predType unitType
boolType :: Type
boolType = primType qBoolId []
predBoolType :: PredType
predBoolType = predType boolType
charType :: Type
charType = primType qCharId []
intType :: Type
intType = primType qIntId []
predIntType :: PredType
predIntType = predType intType
floatType :: Type
floatType = primType qFloatId []
predFloatType :: PredType
predFloatType = predType floatType
stringType :: Type
stringType = listType charType
predStringType :: PredType
predStringType = predType stringType
listType :: Type -> Type
listType ty = primType qListId [ty]
consType :: Type -> Type
consType ty = TypeArrow ty (TypeArrow (listType ty) (listType ty))
ioType :: Type -> Type
ioType ty = primType qIOId [ty]
tupleType :: [Type] -> Type
tupleType tys = primType (qTupleId (length tys)) tys
-- 'numTypes' and 'fractionalTypes' define the eligible types for
-- numeric literals in patterns.
numTypes :: [Type]
numTypes = [intType, floatType]
fractionalTypes :: [Type]
fractionalTypes = drop 1 numTypes
predefTypes :: [(Type, [DataConstr])]
predefTypes =
[ (arrowType a b, [])
, (unitType , [ DataConstr unitId [] ])
, (listType a , [ DataConstr nilId []
, DataConstr consId [a, listType a]
])
]
where a = TypeVariable 0
b = TypeVariable 1