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

hsVar :: Name -> HaskellType

hsApp :: String -> [HaskellType] -> HaskellType

hsForall :: String -> HaskellType -> HaskellType

notAHaskellKind :: MonadTCM tcm => Type -> tcm a

notAHaskellType :: MonadTCM tcm => Type -> tcm a

getHsType :: MonadTCM tcm => QName -> tcm HaskellType

getHsVar :: MonadTCM tcm => Nat -> tcm HaskellCode

isHaskellKind :: Type -> TCM Bool

haskellKind :: MonadTCM tcm => Type -> tcm HaskellKind

haskellType :: MonadTCM tcm => 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.