| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
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 Source
hsKFun :: HaskellKind -> HaskellKind -> HaskellKind Source
hsFun :: HaskellKind -> HaskellKind -> HaskellKind Source
hsVar :: Name -> HaskellType Source
hsApp :: String -> [HaskellType] -> HaskellType Source
hsForall :: String -> HaskellType -> HaskellType Source
notAHaskellKind :: Type -> TCM a Source
notAHaskellType :: Type -> TCM a Source
getHsType :: QName -> TCM HaskellType Source
getHsVar :: Nat -> TCM HaskellCode Source
isHaskellKind :: Type -> TCM Bool Source
haskellKind :: Type -> TCM HaskellKind Source
haskellType :: Type -> TCM HaskellType Source
Note that Inf a b, where Inf is the INFINITY builtin, is
translated to 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.