Safe Haskell | None |
---|
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 = StringSource
hsKFun :: HaskellKind -> HaskellKind -> HaskellKindSource
hsFun :: HaskellKind -> HaskellKind -> HaskellKindSource
hsVar :: Name -> HaskellTypeSource
hsApp :: String -> [HaskellType] -> HaskellTypeSource
hsForall :: String -> HaskellType -> HaskellTypeSource
notAHaskellKind :: Type -> TCM aSource
notAHaskellType :: Type -> TCM aSource
getHsType :: QName -> TCM HaskellTypeSource
getHsVar :: Nat -> TCM HaskellCodeSource
isHaskellKind :: Type -> TCM BoolSource
haskellKind :: Type -> TCM HaskellKindSource
haskellType :: Type -> TCM HaskellTypeSource
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.