variadic functions and typeCast

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
9 messages Options
Reply | Threaded
Open this post in threaded view
|

variadic functions and typeCast

Michael Shulman-3
Hi all,

I am writing, for my own amusement, a more general version of the
trick to implement variadic functions in Haskell outlined at
http://okmij.org/ftp/Haskell/vararg-fn.lhs.  (If someone else has done
this already, please point me to it!)  Code is attached at the end of
the message.  My question concerns the use of `typeCast', which is
defined as follows:

class TypeCast x y | x -> y, y -> x where
    typeCast :: x -> y

instance TypeCast x x where
    typeCast = id

This is taken from the paper "Strongly typed heterogeneous
collections" by Oleg Kiselyov, Ralf Lammel, and Keean Schupke.  As
observed there, the TypeCast instance declaration must occur in a
separate module; otherwise the compiler is too eager about type
simplification.  (I also get the same errors if VarArg is interpreted
by GHCi, even if TypeCast is in a separate module.)  I think I
understand the reason for this, but I find it a little surprising; it
wasn't clear to me from the documentation that fundeps introduce a new
dependence on module boundaries.

Anyway, my main question about typeCast is this: why is it needed here
at all?  If I omit it entirely, the code compiles fine, but then
using it gives error messages like the following:


Prelude VarArg> build 'h' 'i' :: String

<interactive>:1:0:
    No instances for (VarFold [a] [a] [Char], VarAccum Char [a])
      arising from use of `build' at <interactive>:1:0-4
    ...


I don't understand why the type-checker is unable to infer that the
type variable `a' should be specialized to `Char' here, since the only
available instance of VarFold whose third type is [Char] has the first
type also being [Char].  I've given the compiler all the type hints I
can think of.  Can someone explain this to me?

I should say that if I add a functional dependency "l -> a" to the
class VarAccum, then this particular example works.  However, I have
other examples in mind for which l doesn't functionally determine a,
so I don't want to do that.  And I don't see why it's necessary.

Here's the code:


class VarAccum a l where
    accum :: a -> l -> l

class VarFold b l r where
    varFold :: (l -> b) -> l -> r

instance (TypeCast b c) => VarFold b l c where
    varFold f xs = typeCast (f xs)

instance (VarFold b l r, VarAccum a l) => VarFold b l (a -> r) where
    varFold f xs x = varFold f (accum x xs)

-- This is the type of variadic functions from lots of As to a B.
type a :--> b = forall r. (VarFold b [a] r) => r
infixr 0 :-->

instance VarAccum a [a] where
    accum x xs = (x:xs)

varArg :: forall a b. ([a] -> b) -> (a :--> b)
varArg f = varFold (f . reverse) ([] :: [a])

build :: forall a. a :--> [a]
build = varArg (id :: [a] -> [a])


Thanks!
Mike
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: variadic functions and typeCast

oleg-7

Michael Shulman wrote:
> class TypeCast x y | x -> y, y -> x where
>     typeCast :: x -> y
>
> instance TypeCast x x where
>     typeCast = id
>
> Anyway, my main question about typeCast is this: why is it needed here
> at all?

First of all, there is a version of TypeCast that works within the
same module, please see any code described in
        http://pobox.com/~oleg/ftp/Haskell/typecast.html

Appendix D of the full HList paper (or, HList technical report, I
should say) gives the reasons for TypeCast.

Briefly, TypeCast lets us replace a (ground) type T with a type
variable "t" subject to the constraint: "TypeCast t T => t".  The
difference seems superficial since the typechecker can immediately
discharge the constraint and replace "t" with "T". Well, placing the
TypeCast declaration in a different module, or the more convenient
magic 6-line declaration of class TypeCast make sure that the
typechecker delays the discharging of the "TypeCast" constraint.  So
the type variable "t" stays uninstantiated for a while. It matters in
instance declarations. For example,

        class Foo x where foo :: x -> Int
        instance Foo [Int]
        instance Foo Bool where foo x = fromEnum x

If we write
        test1 = foo [read "1"]
we get an error: No instance for (Foo [a]). Indeed, `read "1"' has the
type 'a', which does not match "Int". The typechecker certainly cannot
chose the "Foo [Int]" instance because who knows what other instances
of Foo may occur in other modules. We can tell the typechecker however
that "Foo [Int]" is the only instance that can ever be in the whole
program (that is, the world is `locally' closed, as far as the Foo [a]
is concerned). We do that by writing


        instance TypeCast x Int => Foo [x] where foo [x] = typeCast x
and now
        test1 = foo [read "1"]
typechecks (and works), without any type annotations.

BTW, if we lied and did write another instance for "Foo [T]" for some T,
the typecheker will complain.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: variadic functions and typeCast

Michael Shulman-3
On 9/27/06, [hidden email] <[hidden email]> wrote:
> First of all, there is a version of TypeCast that works within the
> same module, please see any code described in
>         http://pobox.com/~oleg/ftp/Haskell/typecast.html

Yes, I was aware of that; I gave the shorter version just because it's
shorter.  I didn't realize how well-known this TypeCast is, so forgive
my ignorance.

Thanks for your answer.  I think the real point at which I was
confused is that the type-checker never unifies types in order to
*find* an instance of a class, but functional dependencies of a class
can make it unify types.  Thus, by making the instance look more
general but moving the unification into a TypeCast constraint, since
TypeCast has a bidirectional fundep, we can make the instance match a
pair of types that aren't yet unified, and then use TypeCast's fundep
to force their unification.  Is that right?

Mike
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Typeclass vs. Prolog programming

oleg-7

This message is intended as a long answer to Michael Shulman's
question (Re: variadic functions and typeCast) and Jason Dagit's
question (Re: Duplicate Instance problem). Incidentally, the short
answer to Jason Dagit's question is `constraints are disregarded
during instance selection'. The answer to Michael Shulman is yes.

There is a great temptation to read the following declarations

        class Pred a b
        instance (Ord b, Eq b) => Pred [Int] b
        instance Pred Bool Bool

as a Prolog program:

        pred([int],B) <- ord(B),eq(B).
        pred(bool,bool).

(In Prolog, the names of variables are capitalized and the names of
constants begin with a lower-case letter. In Haskell type expressions,
it's the other way around).

There are significant differences between the evaluation of the two
programs. The Prolog evaluator, given a goal 'pred([X],bool)', scans
the rules in their order of appearance, trying to unify the goal with
rule's head.  If successful, the evaluator then tries to solve the
goals in the body of the rule, again strictly in their order of
appearance. On failure, it backtracks. In the above example, the goal
unifies with the head of the first rule, yielding the substitution
{X->int,B->bool}. So, the evaluator will try to solve the goal
ord(bool), and then, if successful, eq(bool). On failure, the
evaluator will try to unify the goal with the fact 'pred(bool,bool)'.
So, Prolog follows the top-to-bottom, left-to-right strategy with
backtracking -- so called SLD resolution.

The evaluation of the typeclass program has two significant
differences. First, there is no backtracking. That makes the
evaluation deterministic, and, furthermore, independent on the order
of the instances and the order of constraints. That is a very good
thing. For comparison, consider XSLT 1.0, Sec 5.5, and the whole mess
with import precedences and priorities. The NodeTest pattern is
assigned the priority -0.5. Naturals are not enough for them.

The second difference from the Prolog evaluation is the use of
matching rather than the full unification when selecting a rule. For
example, the goal "Pred [x] Bool" does _not_ match the head of the
first Pred instance. The type variable 'x' in the goal is not
considered variable during the instance selection.

The absence of backtracking also means that the Haskell typechecker
does not need to consider the constraints when selecting the
instance. If the head of the instance matches the goal, the
typechecker commits to that instance, and only then checks for the
constraints such as Ord b and Eq b in our example. The failure to
(eventually) satisfy these constraints is an unrecoverable type error.

Thus, the following instances in Jason Dagit's question:
        instance Num a       => StringValue a where
        instance RealFloat a => StringValue a where
are identical for the instance selection purposes, where only the
instance head matters.

The absence of backtracking and head-matching rather than the full
unification do not mean that the typeclass language is
deficient. The TypeCast generalizes head-matching to controlled
unification. Indeed, if we write the first instance as

        instance (TypeCast z Int, Ord b, Eq b) => Pred [z] b

then the goal "Pred [x] Bool" will match the head, giving the
substitution {z->x, b->Bool}. The typechecker commits to the instance
and adds to the current constraints
        TypeCast x Int, Ord Bool, Eq Bool
The latter two are obviously satisfied and so discharged. The former
leads to the substitution {x->Int}. So, the net effect is as if we
_unified_ "Pred [x] Bool" with "Pred [Int] b", rather than merely
matched. Compared with Prolog, we have more flexibility: each rule may
specify which of its arguments should be unified against the
corresponding arguments of the goal, and which should be merely
matched.

The backtracking can also be emulated -- but it has to be programmed
explicitly. We have to program the typechecker in the typechecker. That
is not so difficult: the `Smash-your-boilerplate' message essentially
implements the (conventional, backtracking-less) instance resolution
algorithm in the typechecker itself. Please compare gsize in SYB3 with
gsize in `Smash'. The special processing cases in the former are
specified as methods in typeclass instances. With `Smash', exactly the
same information is given in a heterogenous list.  Perhaps the former
is more convenient, but the latter is more flexible as we can add,
inspect, and remove `instances'. The class SApply at the end of the
`Smash' message implements the instance selection algorithm.


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Typeclass vs. Prolog programming

Jason Dagit
On 9/27/06, [hidden email] <[hidden email]> wrote:
>
> This message is intended as a long answer to Michael Shulman's
> question (Re: variadic functions and typeCast) and Jason Dagit's
> question (Re: Duplicate Instance problem). Incidentally, the short
> answer to Jason Dagit's question is `constraints are disregarded
> during instance selection'. The answer to Michael Shulman is yes.

Hmm...Perhaps I'm just sleepy but I read through the descriptions
below and I'm still not sure if what I want to do is easy or extremely
difficult.  I think you're suggesting that I should use something like
TypeCast to control the unification if I want to get rid of my
duplicate instances problem?

I'll re-read this a few times and look at the TypeCast stuff.  I feel
like this is quite a bit over my head at the moment, but your
description is very good and hopefully it will make more sense in the
morning.

Thanks,
Jason
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Duplicate Instance problem

oleg-7

Jason Dagit wrote:

> I tried to create a type class for making instances of Show display a
> custom way.  After using my class for a while I found that sometimes
> RealFloats would display as 'NaN' and this is unacceptable.  So at
> this point I had something like:
>
> class Show a => StringValue a where
>   toString :: a -> String
>
> instance Num a => StringValue a where
>   toString = show
>
> instance RealFloat a => StringValue a where
>   toString x
>     | isNaN x = "" -- as an example
>     | otherwise = show x

The simplest solution: replace the constraint RealFloat with its
members. That is, replace
         "instance RealFloat a => StringValue a"
with

 instance StringValue Float where
   toString x
     | isNaN x = "" -- as an example
     | otherwise = show x

and the same for Double. There are currently only two members of
RealFloat, so code duplication should not be so terrible. Or if it is,
then you can do

> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
> {-# OPTIONS -fallow-overlapping-instances #-}
>
> class Show a => StringValue a where
>   toString :: a -> String
>   toString = show
>
> instance Num a => StringValue a  -- works for all Num except the following
>
> instance StringValue Float where
>   toString = myrealfloatthing
> instance StringValue Double where
>   toString = myrealfloatthing
>
> myrealfloatthing x
>      | isNaN x = "" -- as an example
>      | otherwise = show x
>
> t1 = toString (1::Int)
> t2 = toString (1::Double)
> t3 = toString ((0.0::Double)/0.0)


A more general solution will use generic programming. I doubt however
it will be much shorter than the above.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Typeclass vs. Prolog programming

Michael Shulman-3
In reply to this post by oleg-7
Thank you Oleg!  That explanation is very clear.

On 9/28/06, [hidden email] <[hidden email]> wrote:
> The typechecker commits to the instance
> and adds to the current constraints
>         TypeCast x Int, Ord Bool, Eq Bool
> The latter two are obviously satisfied and so discharged. The former
> leads to the substitution {x->Int}.

By the rules just enumerated, this substitution would be forbidden,
since the type variable x is not considered variable, right?  So this
happens via the magic of functional dependencies?  The typechecker
encounters (eventually) the instance

instance TypeCast'' () x x

and since TypeCast'' is declared with a functional dependency:

class TypeCast'' t x y | t x -> y, t y -> x

it concludes that the first x in the above instance is uniquely
determined by the second, which in our case is Int, and therefore x
must be Int.  Is that right?

This is all very beautiful, but it's a little annoying that the
cornerstone "silver bullet" TypeCast has to be defined in a way that
fools the typechecker into doing the right thing in spite of itself.
Is this all part of the general "fundeps are very hard to get right"
problem?

Mike
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Typeclass vs. Prolog programming

oleg-7

I previously wrote:
> The typechecker commits to the instance
> and adds to the current constraints
>         TypeCast x Int, Ord Bool, Eq Bool
> The latter two are obviously satisfied and so discharged. The former
> leads to the substitution {x->Int}.

I should have been more precise and said:
        The former _eventually_ leads to the substitution {x->Int}.

Your analysis is right on the mark. That's exactly how I think of
TypeCast.


> This is all very beautiful, but it's a little annoying that the
> cornerstone "silver bullet" TypeCast has to be defined in a way that
> fools the typechecker into doing the right thing in spite of itself.

One of the drafts of the HList paper, when describing TypeCast,
literally had a phrase about `fooling the typechecker'...

Well, it seems things like TypeCast were not envisioned by the
Founding Fathers. In this respect, the story of C++ templates come to
mind. My feeling is that we're still discovering the capabilities of
the Haskell typechecker and the right abstractions. We should view
TypeCast as an ungainly _encoding_ of a simple abstraction, or just as
a tool for implementing type-level typecase and local improvement
rules. When the right abstraction emerges (and perhaps it already has:
CHR), GHC might implement it directly. Until then, we can use the
encoding...

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Typeclass vs. Prolog programming

Martin Sulzmann
In reply to this post by oleg-7


[hidden email] writes:
 >
 > There is a great temptation to read the following declarations
 >
 > class Pred a b
 > instance (Ord b, Eq b) => Pred [Int] b
 > instance Pred Bool Bool
 >
 > as a Prolog program:
 >
 > pred([int],B) <- ord(B),eq(B).
 > pred(bool,bool).
 >
 > (In Prolog, the names of variables are capitalized and the names of
 > constants begin with a lower-case letter. In Haskell type expressions,
 > it's the other way around).
 >

Why not simply say that type classes have a natural interpretation
in terms of Constraint Handling Rules (CHRs). For example,
the above instances translate to

rule  Pred [Int] <==> Ord b, Eq b
rule  Pred Bool Bool <==> True

CHRs specify rewrite rules among constraints (from left to right).
A CHRs fires if we find a constraint which matches the left hand
side (compare this to Prolog where we use unification).

Why CHRs are great for reasoning about type classes is well-documented
here:
http://www.comp.nus.edu.sg/~sulzmann/research/node4.html

Martin
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe