Recursive Type Representatives Using GADTs

user_11838776 0
Viewed 113

I have the following GADT which can represent basic algebraic data types.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}

data Type :: * -> * where
  TUnit   :: Type ()
  TInt    :: Type Int
  (:+)    :: Type a -> Type b -> Type (Either a b)
  (:*)    :: Type a -> Type b -> Type (a, b)
  (:>)    :: Type a -> Type b -> Type (a -> b)
deriving instance Show (Type a)

I can use it along with the following GADT to create values with types available at runtime.

data Value where
  MkVal :: a -> Type a -> Value

someVal = MkVal (+) (TInt :> (TInt :> TInt))

This works well for non-recursive types, but I would also like to include other types like lists and trees without adding them in manually. A type constructor could be represented as a function Type a -> Type b, for example, maybeConstr a = TUnit :+ a. However, I cannot turn this into a recursive definition of Nat. Using fix doesn't work because the input and output types don't match up. Also, representing type constructors as functions seems like it could be problematic if I want to write an equality function for types. Is there a good way to accomplish this?

recursive-type gadt haskell
1 Answers

You can represent a recursive type using a fixed point, by adding a constructor TMu to represent the recursive type μx. t. This is a type that can be “unrolled” into the type t with x replaced with another copy of μx. t: t[μx. t/x]. For example, the list type could be written as L(a) = μx. 1 + a × x; the type variable x represents the whole type L(a). (Technically this is the greatest fixed point ν, and μ is the least fixed point, but it’s common to use μ for both if we don’t care about the distinction.)

In order to use this, you will need some representation of type variables; a general-purpose way to represent this with your typed AST is to include the type of the “environment” among the type parameters of the GADT, and index into that environment with De Bruijn indices.

data Type :: [*] -> * -> * where
  TUnit   :: Type c ()
  TInt    :: Type c Int
  (:+)    :: Type c a -> Type c b -> Type c (Either a b)
  (:*)    :: Type c a -> Type c b -> Type c (a, b)
  (:>)    :: Type c a -> Type c b -> Type c (a -> b)

  TMu     :: Type (a ': c) b -> Type c (Mu a b)
  TVarZ   :: Type (a ': c) a
  TVarS   :: Type c a -> Type (x ': c) a

TVarZ references the variable at the top of the environment stack, and TVarS shifts the context to refer to other parts of the environment. If you will never need nested recursive types, you can get away without TVarS, and call TVarZ something like TSelf or TRec instead.

Formally, this makes each constructor of the GADT correspond to a rule of the type system that you’re representing: Type γ α → Type γ β → Type γ (α × β) corresponds directly to the sequent (Γ ⊢ α) ∧ (Γ ⊢ β) ⇒ (Γ ⊢ α × β).

If you want to be able to represent type constructors within Type, the process is similar: Maybe a ≅ 1 + a can also be thought of as Maybe ≅ ∀a. 1 + a, where ∀ here is much like λ at the term level. So you would need to add TForall and TApp constructors to Type, and use the TVar constructors to refer to the variables they bind.

This raises two issues. First, you need to consider kinds now, too, although you don’t need to represent them explicitly if your type parameters are all basic types (i.e. not type constructors). Second, you’re currently indexing the GADT with Haskell types directly, but you will run into issues using TForall :: Type (a ': c) b -> Type c (forall a. b) directly; a typical solution is to create a basic “untyped” version of your AST type:

data UType where
  UTUnit   :: UType
  UTInt    :: UType
  UTSum    :: UType -> UType -> UType
  UTProd   :: UType -> UType -> UType
  UTFun    :: UType -> UType -> UType

Then data Type :: * -> * becomes data Type :: UType -> *, using DataKinds:

data Type :: * -> * where
  TUnit   :: Type 'UTUnit
  TInt    :: Type 'UTInt
  (:+)    :: Type a -> Type b -> Type ('UTSum a b)
  (:*)    :: Type a -> Type b -> Type ('UTProd a b)
  (:>)    :: Type a -> Type b -> Type ('UTFun a b)

(And this is basically the “singleton” form of UType.)

You would then extend this for the above cases, and have an interpretation to and from Haskell types.

The De Bruijn representation makes it easy to derive equality on Types, but there are several possible representations of variable binding here, such as variable names, “locally nameless”, “higher-order abstract syntax” (HOAS), or using point-free type combinators only.

user_2468860
Related