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

Safe Haskell | None

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

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.