Existential Data Constructors in Haskell and Qi
In Haskell, if we have a type A and a set of functions from A to some other type, we may wish to encapsulate this logic inside of a new general type that does not contain a reference to A. We would like to be able to pass different data and functions to this type constructor and have the dependent functions work across all types, given a proper datatype for our function and data that matches that datatype. Haskell calls this pattern "Existential Data Construction."In A History of Haskell: Being Lazy With Class , Hudak, Hughes, Wadler, and Jones provide the following Haskell datatype as motivation for existential data constructors.
data T = forall a. MkT a (a->Int)
f :: T -> Int
f (MkT x g) = g x
Reading this type is fairly straight forward. We say that for any type a, we can call a constructor consisting of a value of that type and a function from type a -> Int and get a type T back. F then takes this supplied T value and uses pattern matching to deconstruct it and forces the call of G on X. Given that G is of type (a->Int) and X is of type a, we can be certain this call will work.
I'm belaboring this point because I think it is important to understand that the Qi type system has this expressive power without requiring a (forall a) existential constructor in the type. In Qi, we can simply specify some generic type A on the right hand side of the type colon around a variable bound below the sequent refinement rule and rest assured that the type theory will deduce the existence of and proper type for A at compile time.
Here is how T looks inside of Qi.
(datatype t
X : A;
L : (A --> number);
======
(@p mk_t (@p X L)) : t;
)
We can read this as saying, "If I need to prove something is of type t I must first prove that it is a constructor that has an X of some arbitrary type A and a function L of type A --> number."
From there, we can define the function f in a similar manner as the Haskell code.
(define f
{ t --> number }
(@p mk_t (@p X G)) -> (G X))
Running this shows how the type system ensures that the A's match up inside the constructor.
(3+) (f (@p mk_t (@p 3 (+ 4))))
7 : number
(4+) (f (@p mk_t (@p a (+ 4))))
error: type error
Like in Haskell, this existential datatype constructor truly covers all types A, as I will show below. In the following code, the type A is bound to (number --> number). Qi, like Haskell, really means it when it says, "any type A".
(7+) (/. X (+ X 3))
#function :LAMBDA [X] [+ X 3] : (number --> number)
(8+) (f (@p mk_t (@p (/. X (+ X 3))
(/. Y (Y 7)) )) )
10 : number
I hope this explanation helps further the understanding of the Qi type system for Haskell users interested in Qi. Feel free to ask any questions you may have.
0 Comments:
