Is it possible to express the type of (Type,Value) pairs on Haskell?

Question

Lists of (Type,Value) pairs can be expressed on Idris as:

data List : Type where
  Cons : (t : Type ** t) -> List -> List
  Nil  : List

example : List
example = Cons (Nat ** 3) (Cons (Bool ** True) Nil)

What is the syntax to express those on Haskell?

Answer 1

Note that if you construct such List you cannot do anything with the elements, as you cannot pattern match on the types.

However it's entirely possible in Haskell usign GADTs

data List where
    Cons :: t -> List -> List
    Nil  :: List

example :: List
example = Cons (3 :: Int) (Cons True Nil)

You can extend that with a constraint, e.g. Typeable so you get run-time type information to do things on elements in the list:

data CList (c :: * -> Constraint) where
    CCons :: Typeable t => t -> List c -> List c
    CNil  :: CList c

exampleC :: CList Typeable
exampleC = CCons (3 :: Int) (CCons True CNil)

Or you can use HList

data HList (xs :: [*]) where
    HCons :: x -> List xs -> List (x ': xs)
    HNil  :: '[]

exampleH :: HList '[Int, Bool]
exampleH = HCons 3 (HConst True HNil)

---

In particular dependent pairs (or sums!) (Idris docs) are possible with in Haskell to, Yet we have to make a GADT for a function! The http://hackage.haskell.org/package/dependent-sum is one many use

If Idris version is

data DPair : (a : Type) -> (P : a -> Type) -> Type where
   MkDPair : {P : a -> Type} -> (x : a) -> P x -> DPair a P

the Haskell is not that much different when a = Type:

data DPair (p :: * -> *) where
   MkDPair :: p a -> DPair p

and p is encoded with a GADT. In examples above, it's sliced into the definitions.

You can also make dependent pairs with something else than a type as a first element. But then you have to read about singletons.