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.
In my studies of Qi, I often use Haskell as an endless pool for mining good ideas. I find that by translating these ideas into Qi, I end up learning both Qi and Haskell better than I would have done by trying to understand them separately. For example, I was immediately able to understand that "Multi-parameter Type Classes with Undecidable instances" was really just "Sequents with bad syntax." But one area that Haskell reigns supreme is the Type Class.
Qi does have a sub-classing mechanism. If you define a type under the universal truth that
(subtype integer number) then you can define a type rule that says
(subtype B A); X : B;
_____________________
X : A;
and integers can now go wherever numbers go. Basically, it is a promise to the compiler that you are REALLY sure the implementations of the types match up and all the proper functions have been provided. Honest. You promise... That tends to fail in practice. And this sub-classing system does not provide any ability to do ad hoc polymorphism.
The Haskell idea is to use special syntax to pass around a hidden object that carries all of the required functions and is properly typed. They call this a Type Class. It is an incredibly handy feature because it provides a way to guarantee that you have met the basic needs of a function that requires the type class. It also allows function overloading, a feature Qi lacks.
So how would this feature look if ported inside of Qi? I would imagine it would looks something like the following code snippet. Note that the "class_" prefix on * is due to Qi not allowing the redefinition of operators. I'll use that notation convention throughout, as I rebuild the (num N) class in Qi.
(define square
{ (num N) ==> N --> N }
X -> (class_* X X))
The meaning of the statement is the same as Haskell. If I have a (num N) class then I can use the class_* to call the proper function. Internally, Qi would transform this construct into the following along the same manner as Haskell.
(define square
{ (num N) --> N --> N }
D X -> (num_* D X X))
The code to perform this transformation will not be provided. This code would have to be intimately tied into the type system and would require a very large change to Qi. It may be worth it, but it is not the point of this article. I will perform the transformation by hand and demonstrate from there.
For the purposes of this article, I will be providing the base types integer and float. They both have their own type specific operations. I will create instances of them into the (num N) class which will also propagate that instance to the subtype (eq N).
Haskell defines the EQ class as
class Eq a where
(==), (/=) :: a -> a -> Bool
Haskell hides the creation of the constructor type for EQ, but in the final transformation it gets an explicit expression inside the compiler. The final transformation should create both a new Qi datatype and some new generic functions that the type class requires. I provide the transformation in Qi below.
(datatype eq
Equal : (A --> (A --> boolean));
NotEqual : (A --> (A --> boolean));
===
(@p mkeq (@p Equal NotEqual)) : (eq A);
)
(define class_equal
{ (eq N) --> N --> N --> boolean }
(@p mkeq (@p Equal _))
X Y -> (Equal X Y))
(define class_notequal
{ (eq N) --> N --> N --> boolean }
(@p mkeq (@p _ NotEqual))
X Y -> (NotEqual X Y))
As you can see, the idea is to pass along the proper EQ object for the function type and use pattern matching to splice in the arguments and the proper function and then call it. Getting this transformation to take arbitrary code and make these datatypes and functions requires most of the work. The final result can work as these hand written functions do, but a real implementation would structure things differently.
The instance declaration in Haskell looks something like the following
instance Eq Integer where
x == y = x `integerEq` y
instance Eq Float where
x == y = x `floatEq` y
The final transformation of the Qi code would look like the following snippet. It provides the needed functions for the type class by taking the type specific functions and putting them into a type class container. This is the same container that we send to every function that requires a type class. All we need to do is provide the base implementations in the proper spots. In a full Qi type class implementation, we would have to use some special syntax or data structure to cause these functions to auto-generate themselves.
(define instance-eq-integer
{ A --> (eq integer) }
_ -> (@p mkeq (@p equal-integer notequal-integer)))
(define instance-eq-float
{ A --> (eq float) }
_ -> (@p mkeq (@p equal-float notequal-float)))
When we run the code, it behaves as expected.
(39+) (class_equal (instance-eq-float 0) 2.3 2.3)
true : boolean
(40+) (class_equal (instance-eq-float 0) 2.3 2.4)
false : boolean
(41+) (class_equal (instance-eq-integer 0) 2 2)
true : boolean
(42+) (class_equal (instance-eq-float 0) 2.0 2)
error: type error
Notice that line 42 fails. To perform this kind of analysis, we will need a type class that captures both equality and the idea of being a number, with a way to translate them from the integers. Haskell defines the (num N) type in a way very close to the form below.
class (Eq a) => Num a where
(+), (-), (*) :: a -> a -> a
negate :: a -> a
abs, signum :: a -> a
fromInteger :: Integer -> a
We can define an equivalent structure in Qi by embedding the eq subclass directly into the mknum structure. The compiler would also need to provide a function to walk the subclass tree.
(datatype num
Subclass : (eq A);
Plus : (A --> (A --> A));
Minus : (A --> (A --> A));
Mult : (A --> (A --> A));
Neg : (A --> A);
Abs : (A --> A);
SigNum : (A --> A);
FromInteger : (integer --> A);
===
(@p
Subclass
(@p mknum (@p Plus
(@p Minus
(@p Mult
(@p Neg
(@p Abs
(@p SigNum FromInteger)))))))) : (num A);
)
(define num_to_eq
{(num N) --> (eq N)}
(@p
(@p mkeq (@p E Ne))
(@p mknum (@p _
(@p _
(@p _
(@p _
(@p _
(@p _ _)))))))) -> (@p mkeq (@p E Ne)))
The basic function definitions work like equal type class from above.
(define class_*
{ (num N) --> N --> N --> N }
(@p
_
(@p mknum (@p Plus
(@p Minus
(@p Mult
(@p Neg
(@p Abs
(@p SigNum FromInteger))))))))
X Y -> (Mult X Y))
And we declare the instance by providing all of the functions in their proper slots.
(define instance-num-integer
{ A --> (num integer) }
_ ->
(@p
(instance-eq-integer 0)
(@p mknum (@p plus-integer
(@p minus-integer
(@p mult-integer
(@p neg-integer
(@p abs-integer
(@p signum-integer frominteger-integer)))))))) )
(define instance-num-float
{ A --> (num float) }
_ ->
(@p
(instance-eq-float 0)
(@p mknum (@p plus-float
(@p minus-float
(@p mult-float
(@p neg-float
(@p abs-float
(@p signum-float frominteger-float)))))))) )
So now we have what we need to take on 2.0 == 2.
(class_equal (num_to_eq (instance-num-float 0))
2.0
(class_frominteger (instance-num-float 0) 2))
true : boolean
If we encapsulate that into a function 'istwo?' we can see the transformation a bit more clearly.
(define istwo?
{ (num N) --> N --> boolean }
D X -> (class_equal (num_to_eq D) (class_frominteger D 2) X))
istwo? : ((num A) --> (A --> boolean))
(10+) (istwo? (instance-num-integer 0) 2)
true : boolean
(11+) (istwo? (instance-num-integer 0) 3)
false : boolean
(12+) (istwo? (instance-num-float 0) 2.0)
true : boolean
Ideally, the above 'istwo?' function should be auto-generated by the following Qi like code. Note that the type system would wrap the small constants in frominteger and call the subclass datatype return function to make a valid class_equal call.
(define istwo?
{ (num N) ==> N --> boolean }
X -> (class_equal 2 X))
To finish, I'll implement squares and sumsquares that work across the type class (num N).
(define square
{ (num N) --> N --> N }
D X -> (class_* D X X))
(define sumsquares
{ (num N) --> N --> N }
D X -> (class_+ D (square D X)
(square D X)))
(16+) (square (instance-num-float 0) 6.0)
36.0 : float
(17+) (square (instance-num-integer 0) 2)
4 : integer
(18+) (sumsquares (instance-num-integer 0) 2)
8 : integer
(19+) (sumsquares (instance-num-float 0) 6.0)
72.0 : float
In short, type classes are a very powerful programming tool that Qi lacks and should probably have. They give Qi ad hoc polymorphism and define types that also have guarantees about which functions it supports. It would take a fairly large change to the Qi codebase to support the shorthand syntax, but I hope this article has proven that we can implement the powerful Haskell type system in Qi.
Thank you for your time.
Download the full code used to make this article.
