Is it possible to express the type (type, value) of a pair in Haskell?

Question

Lists of pairs (Type, Value) 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 of an expression for Haskell?

Answer 1

Please note: if you build such a List , you cannot do anything with the help of elements, since you cannot match type matches.

However, this is 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 this with a restriction, for example. Typeable so that you have runtime information to execute items 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 in Haskell, But we have to do a GADT for the function! http://hackage.haskell.org/package/dependent-sum is a lot of good

If the version of Idris

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

Haskell is not much different with a = Type :

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

and p is encoded using GADT . In the above examples, he cut into definitions.

You can also create dependent pairs with something other than the type as the first element. But then you should read about singletons .