Agda.Compiler.HaskellTypes

Translating Agda types to Haskell types. Used to ensure that imported Haskell functions have the right type.

Documentation

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

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.