{- | Type definitions -} {-# language OverloadedStrings #-} module Language.Giml.Types.Types where import Data.Foldable (foldl') import Language.Giml.Common import Data.Data (Data) -- | A data type representing types data Type = TypeVar TypeVar -- ^ type variables, like @a@ | TypeCon TypeCon -- ^ type constructors, like @List@ and @Int@ | TypeApp Type Type -- ^ type application, like @List a@ | TypeRec [(Label, Type)] -- ^ the type of a record, like @{ x : Int, y : String }@ | TypeRecExt [(Label, Type)] TypeVar -- ^ a record with an extension, such as @{ x : Int, y : String | r }@, -- means "this record has at least @{ x : Int, y : String }@, but can have more fields" | TypeVariant [(Constr, Type)] -- ^ the type of a closed variant, such as @[ Some : Int | Nil : {} ]@, -- the value can be one of the constructors. | TypePolyVariantLB [(Constr, Type)] TypeVar -- ^ the type of a lower bounded polymorphic variant, such as @[a> Some : Int | Nil : {} ]@, -- the value can be at least one of the constructors or potentially more. | TypePolyVariantUB TypeVar [(Constr, Type)] -- ^ the type of a upper bounded polymorphic variant, such as @[a< Some : Int | Nil : {} ]@, -- the value can be at most one of the constructors or potentially less. -- -- The type variable here is special and is used to track the information of -- which variants we already know of during the type inference process. | TypeScheme [TypeVar] Type -- ^ A generalized type which closes over all of its type variables, -- such as @forall a b. a -> b -> a@ deriving (Int -> Type -> ShowS [Type] -> ShowS Type -> String (Int -> Type -> ShowS) -> (Type -> String) -> ([Type] -> ShowS) -> Show Type forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Type] -> ShowS $cshowList :: [Type] -> ShowS show :: Type -> String $cshow :: Type -> String showsPrec :: Int -> Type -> ShowS $cshowsPrec :: Int -> Type -> ShowS Show, Type -> Type -> Bool (Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Type -> Type -> Bool $c/= :: Type -> Type -> Bool == :: Type -> Type -> Bool $c== :: Type -> Type -> Bool Eq, Eq Type Eq Type -> (Type -> Type -> Ordering) -> (Type -> Type -> Bool) -> (Type -> Type -> Bool) -> (Type -> Type -> Bool) -> (Type -> Type -> Bool) -> (Type -> Type -> Type) -> (Type -> Type -> Type) -> Ord Type Type -> Type -> Bool Type -> Type -> Ordering Type -> Type -> Type forall a. Eq a -> (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: Type -> Type -> Type $cmin :: Type -> Type -> Type max :: Type -> Type -> Type $cmax :: Type -> Type -> Type >= :: Type -> Type -> Bool $c>= :: Type -> Type -> Bool > :: Type -> Type -> Bool $c> :: Type -> Type -> Bool <= :: Type -> Type -> Bool $c<= :: Type -> Type -> Bool < :: Type -> Type -> Bool $c< :: Type -> Type -> Bool compare :: Type -> Type -> Ordering $ccompare :: Type -> Type -> Ordering Ord, Typeable Type Typeable Type -> (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type -> c Type) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type) -> (Type -> Constr) -> (Type -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Type)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)) -> ((forall b. Data b => b -> b) -> Type -> Type) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r) -> (forall u. (forall d. Data d => d -> u) -> Type -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> Type -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Type -> m Type) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type) -> Data Type Type -> DataType Type -> Constr (forall b. Data b => b -> b) -> Type -> Type forall a. Typeable a -> (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> Type -> u forall u. (forall d. Data d => d -> u) -> Type -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Type -> m Type forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type -> c Type forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Type) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type) gmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type gmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type gmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Type -> m Type $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Type -> m Type gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Type -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Type -> u gmapQ :: forall u. (forall d. Data d => d -> u) -> Type -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Type -> [u] gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r gmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r gmapT :: (forall b. Data b => b -> b) -> Type -> Type $cgmapT :: (forall b. Data b => b -> b) -> Type -> Type dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type) dataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Type) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Type) dataTypeOf :: Type -> DataType $cdataTypeOf :: Type -> DataType toConstr :: Type -> Constr $ctoConstr :: Type -> Constr gunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type gfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type -> c Type $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type -> c Type Data) typeFun :: [Type] -> Type -> Type typeFun :: [Type] -> Type -> Type typeFun [Type] argsT Type retT = (Type -> Type -> Type) -> Type -> [Type] -> Type forall (t :: * -> *) a b. Foldable t => (a -> b -> b) -> b -> t a -> b foldr (\Type i Type o -> Type -> Type -> Type TypeApp (Type -> Type -> Type TypeApp (TypeCon -> Type TypeCon TypeCon "->") Type i) Type o) Type retT [Type] argsT typeApp :: Type -> [Type] -> Type typeApp :: Type -> [Type] -> Type typeApp = (Type -> Type -> Type) -> Type -> [Type] -> Type forall (t :: * -> *) b a. Foldable t => (b -> a -> b) -> b -> t a -> b foldl' Type -> Type -> Type TypeApp toTypeFun :: Type -> ([Type], Type) toTypeFun :: Type -> ([Type], Type) toTypeFun = \case TypeApp (TypeApp (TypeCon TypeCon "->") Type i) Type o -> let ([Type] f, Type r) = Type -> ([Type], Type) toTypeFun Type o in (Type i Type -> [Type] -> [Type] forall a. a -> [a] -> [a] : [Type] f, Type r) Type other -> ([], Type other)