Haskell-like Type Classes in Qi
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.
0 Comments:
