Safe Haskell | None |
---|
Agda.Compiler.HaskellTypes
Description
Translating Agda types to Haskell types. Used to ensure that imported Haskell functions have the right type.
- type HaskellKind = String
- hsStar :: HaskellKind
- hsKFun :: HaskellKind -> HaskellKind -> HaskellKind
- hsFun :: HaskellKind -> HaskellKind -> HaskellKind
- hsUnit :: HaskellType
- hsVar :: Name -> HaskellType
- hsApp :: String -> [HaskellType] -> HaskellType
- hsForall :: String -> HaskellType -> HaskellType
- notAHaskellKind :: Type -> TCM a
- notAHaskellType :: Type -> TCM a
- getHsType :: QName -> TCM HaskellType
- getHsVar :: Nat -> TCM HaskellCode
- isHaskellKind :: Type -> TCM Bool
- haskellKind :: Type -> TCM HaskellKind
- haskellType :: Type -> TCM HaskellType
Documentation
type HaskellKind = String
hsKFun :: HaskellKind -> HaskellKind -> HaskellKind
hsFun :: HaskellKind -> HaskellKind -> HaskellKind
hsVar :: Name -> HaskellType
hsApp :: String -> [HaskellType] -> HaskellType
hsForall :: String -> HaskellType -> HaskellType
notAHaskellKind :: Type -> TCM a
notAHaskellType :: Type -> TCM a
getHsType :: QName -> TCM HaskellType
getHsVar :: Nat -> TCM HaskellCode
isHaskellKind :: Type -> TCM Bool
haskellKind :: Type -> TCM HaskellKind
haskellType :: Type -> TCM HaskellType
Note that Inf a b
, where Inf
is the INFINITY builtin, is
translated to translation of b
(assuming that all coinductive
builtins are defined).
Note that if haskellType
supported universe polymorphism then the
special treatment of INFINITY might not be needed.