-- | The basis of the Nix type system (type-level).
--   Based on the Hindley–Milner type system.
--   Therefore -> from this the type inference follows.
module Nix.Type.Type where

import           Nix.Prelude                 hiding ( Type, TVar )
import           Nix.Expr.Types

-- | Hindrey-Milner type interface

-- | Type variable in the Nix type system.
newtype TVar = TV Text
  deriving (Int -> TVar -> ShowS
[TVar] -> ShowS
TVar -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TVar] -> ShowS
$cshowList :: [TVar] -> ShowS
show :: TVar -> String
$cshow :: TVar -> String
showsPrec :: Int -> TVar -> ShowS
$cshowsPrec :: Int -> TVar -> ShowS
Show, TVar -> TVar -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TVar -> TVar -> Bool
$c/= :: TVar -> TVar -> Bool
== :: TVar -> TVar -> Bool
$c== :: TVar -> TVar -> Bool
Eq, Eq TVar
TVar -> TVar -> Bool
TVar -> TVar -> Ordering
TVar -> TVar -> TVar
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 :: TVar -> TVar -> TVar
$cmin :: TVar -> TVar -> TVar
max :: TVar -> TVar -> TVar
$cmax :: TVar -> TVar -> TVar
>= :: TVar -> TVar -> Bool
$c>= :: TVar -> TVar -> Bool
> :: TVar -> TVar -> Bool
$c> :: TVar -> TVar -> Bool
<= :: TVar -> TVar -> Bool
$c<= :: TVar -> TVar -> Bool
< :: TVar -> TVar -> Bool
$c< :: TVar -> TVar -> Bool
compare :: TVar -> TVar -> Ordering
$ccompare :: TVar -> TVar -> Ordering
Ord)

-- | The basic type definitions in the Nix type system (type-level code).
data Type
  = TVar TVar                -- ^ Type variable in the Nix type system.
  | TCon Text                -- ^ Concrete (non-polymorphic, constant) type in the Nix type system.
  | TSet Variadic (AttrSet Type) -- ^ Heterogeneous map in the Nix type system. @True@ -> variadic.
  | TList [Type]             -- ^ Heterogeneous list in the Nix type system.
  | (:~>) Type Type          -- ^ Type arrow (@Type -> Type@) in the Nix type system.
  | TMany [Type]             -- ^ Variant type (term). Since relating to Nix type system, more precicely -
                             --   dynamic types in dynamicly typed language (which is Nix).
  deriving (Int -> Type -> ShowS
[Type] -> ShowS
Type -> String
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
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
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)

infixr 1 :~>

-- | Hindley–Milner type system uses "scheme" term for "polytypes".
--   Types containing @forall@ quantifiers: @forall a . a@.
--   Note: HM allows only top-level @forall@ quantification, so no @RankNTypes@ in it.
data Scheme = Forall [TVar] Type -- ^ @Forall [TVar] Type@: the Nix type system @forall vars. type@.
  deriving (Int -> Scheme -> ShowS
[Scheme] -> ShowS
Scheme -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Scheme] -> ShowS
$cshowList :: [Scheme] -> ShowS
show :: Scheme -> String
$cshow :: Scheme -> String
showsPrec :: Int -> Scheme -> ShowS
$cshowsPrec :: Int -> Scheme -> ShowS
Show, Scheme -> Scheme -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Scheme -> Scheme -> Bool
$c/= :: Scheme -> Scheme -> Bool
== :: Scheme -> Scheme -> Bool
$c== :: Scheme -> Scheme -> Bool
Eq, Eq Scheme
Scheme -> Scheme -> Bool
Scheme -> Scheme -> Ordering
Scheme -> Scheme -> Scheme
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 :: Scheme -> Scheme -> Scheme
$cmin :: Scheme -> Scheme -> Scheme
max :: Scheme -> Scheme -> Scheme
$cmax :: Scheme -> Scheme -> Scheme
>= :: Scheme -> Scheme -> Bool
$c>= :: Scheme -> Scheme -> Bool
> :: Scheme -> Scheme -> Bool
$c> :: Scheme -> Scheme -> Bool
<= :: Scheme -> Scheme -> Bool
$c<= :: Scheme -> Scheme -> Bool
< :: Scheme -> Scheme -> Bool
$c< :: Scheme -> Scheme -> Bool
compare :: Scheme -> Scheme -> Ordering
$ccompare :: Scheme -> Scheme -> Ordering
Ord)

-- | Concrete types in the Nix type system.
typeNull, typeBool, typeInt, typeFloat, typeString, typePath :: Type
typeNull :: Type
typeNull   = Text -> Type
TCon Text
"null"
typeBool :: Type
typeBool   = Text -> Type
TCon Text
"boolean"
typeInt :: Type
typeInt    = Text -> Type
TCon Text
"integer"
typeFloat :: Type
typeFloat  = Text -> Type
TCon Text
"float"
typeString :: Type
typeString = Text -> Type
TCon Text
"string"
typePath :: Type
typePath   = Text -> Type
TCon Text
"path"

-- This models a set that unifies with any other set.
typeSet :: Type
typeSet :: Type
typeSet = Variadic -> AttrSet Type -> Type
TSet forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty

typeList :: Type
typeList :: Type
typeList = [Type] -> Type
TList forall a. Monoid a => a
mempty

typeFun :: NonEmpty Type -> Type
typeFun :: NonEmpty Type -> Type
typeFun (Type
head_ :| [Type]
tail_) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
(:~>) Type
head_ [Type]
tail_