HasHsType.agda

module Class.HasHsType where

open import Level using (Level)
open import Data.Bool.Base using (Bool)
open import Data.Nat.Base using (ℕ)
open import Data.String.Base using (String)
open import Data.List.Base using (List)
open import Data.Maybe.Base using (Maybe)
open import Data.Sum.Base using (_⊎_)
open import Data.Product.Base using (_×_)
open import Data.Unit using (⊤)

open import Foreign.Haskell.Pair using (Pair)
open import Foreign.Haskell.Either using (Either)

private variable
  l : Level
  A B : Set l

record HasHsType (A : Set l) : Set₁ where
  field
    HsType : Set

HsType : (A : Set l) → ⦃ HasHsType A ⦄ → Set
HsType _ ⦃ i ⦄ = i .HasHsType.HsType

MkHsType : (A : Set l) (Hs : Set) → HasHsType A
MkHsType A Hs .HasHsType.HsType = Hs

instance

  iHsTy-ℕ      = MkHsType ℕ ℕ
  iHsTy-Bool   = MkHsType Bool Bool
  iHsTy-⊤      = MkHsType ⊤ ⊤
  iHsTy-String = MkHsType String String

  -- Could make a macro for these kind of congruence instances.
  iHsTy-List : ⦃ HasHsType A ⦄ → HasHsType (List A)
  iHsTy-List {A = A} .HasHsType.HsType = List (HsType A)

  iHsTy-Maybe : ⦃ HasHsType A ⦄ → HasHsType (Maybe A)
  iHsTy-Maybe {A = A} .HasHsType.HsType = Maybe (HsType A)

  iHsTy-Fun : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A → B)
  iHsTy-Fun {A = A} {B = B} .HasHsType.HsType = HsType A → HsType B

  iHsTy-Sum : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A ⊎ B)
  iHsTy-Sum {A = A} {B = B} .HasHsType.HsType = Either (HsType A) (HsType B)

  iHsTy-Pair : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A × B)
  iHsTy-Pair {A = A} {B = B} .HasHsType.HsType = Pair (HsType A) (HsType B)