Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda.Compiler.HaskellTypes

Description

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

Synopsis

- 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

# 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.