Keean wrote:

Not saying it isn't tricky - but thats what the HList library (http://www.cwi.nl/~ralf/HList) implements, a heterogenous list. It works slightly differently using classes, but does abstract the workings enough to be useful, to construct an HList you can do:

hlist = "a" .*. (3:Int) .*. False .*. 'v' .*. HNil

And provides head/tail functions and other useful list and set operators.

Keean.

Phew, not bad, but not easy to absorb. Do you know whether the Joy Combinators would work with HList? If I find the time, I'll try to see for myself tomorrow, but I'm not sure that I will. Respectfully, Daniel

Am Montag, 7. März 2005 17:58 schrieb Greg Buchholz:

Daniel Fischer wrote:

...

Am Freitag, 4. März 2005 19:35 schrieb Greg Buchholz:

...

So, can anyone direct me towards more information on exactly what an "Occurs check" is, or does anyone see an easy fix to my problems?

If I remember correctly, an "occurs check" is checking whether a type variable (call it 't') occurs as an argument to a tuple constructor or function arrow in a type expression to be substituted for t, as above or in t = t -> t1.

Such occurences would lead to an infinite type, hence are forbidden.

Interesting, I'll have to think it over. (Of course being a relative newcomer to Haskell, I have to do a lot of thinking when it comes to most things.) BTW, can anyone recommend a good introductory resource for learning about type theory? I once flipped through Pierce's Types_and_Programming_Languages, but at first glance, it seemed to be a little advanced for my understanding (the foreign-looking equations per word ratio seemed a little too high).

...

I have a fix for the factorial and similar recursive functions, though it's not really easy (and needs extensions): don't define the recursion combinators via Stack, do it like this:

linrec2 :: forall a. (forall b. (a,(a,b)) -> (a,b)) -> (forall b. (a,b) -> (a,(a,b))) -> (forall b. (a,b) -> (a,b)) -> (forall b. (a,b) -> (Bool,b)) -> (forall b. (a,b) -> (a,b)) linrec2 rec2 rec1 t p stack

| fst $ p stack = t stack | otherwise = rec2 $ linrec2 rec2 rec1 t p (rec1 stack)

Nice. Definitely something for me to study. Of course, IFAICT, the main motivation for Joy is to try and define everything in terms of function composition instead of function application.

One more, you need not supply a type signature for fact, if you provide the argument: fact0 (n,st) = ifte (dup ! pre ! fact ! mult, (pop ! lit 1, (nul, (n,st)))) That's of course rather "unJoyful" :-), but it helps the type-checker (I don't know the workings thereof, but it's often the case that functions which don't type-check points-free do if sufficiently many arguments are provided). I don't think that'll help fact3-5, though.

...

I don't know Joy, but probably there the stack is (roughly) a heterogenous list, which is hard to model in Haskell,

Yeah, I don't know Joy either, other than reading a few documents,

I've taken a look, and I must say, I find Haskell more intuitive.

but I do think its stack is really heterogenous list. The one reason I was thinking this might be doable in Haskell, is the fact that the few combinators I looked at don't recurse down the whole "stack". That, of

I think, it would be possible to define recursion combinators for specific patterns, like this functions takes 4 elements from the stack, this one 3 and so on, but then you would need combinators for all these patterns, which is rather cumbersome. IMO, it's just not the thing to do things in Haskell exactly like in Joy (or in Java, prolog, or - horribile dictu- in C/C++). Even if it's possible, the spirit of the languages is so different that you should do the same thing in different ways. But of course it's interesting to see whether it can be done.

course, would be a complete nightmare in Haskell. Instead they take a "stack", munge a few (finite number of) items at the top, and return

That's nightmarish enough, because Haskell is strongly typed. So, if we look at linrec, for example, we find that rec2 and rec1 must return the same type as they devour, that's why fact5 doesn't work, because mult has type Num a => (a,(a,b)) -> (a,b). And, BTW, that's why Keean et al's HList library doesn't help here either, the type of an HList determines the number of elements and the type of each, so there we face the same problems as with nested tuples. What we need is type Stack = [ArbitraryType] (from the HList paper, I surmise that [Dynamic] would be possilble, but that seems to have it's own problems).

another "stack". I was hoping that the type variable "a" in (Integer, a) -> (Integer, a) would be amorphous enough to match whatever was left over after grabbing a few items off the top of this "stack".

Well, it's fairly amorphous, but it must be the same type in both type-expressions, and that's why the points-free definition of fact doesn't type-check without the type signature, the 'fact' in the else-branch is used at type (Integer,(Integer,a)) and so on, without the type signature, the type-checker assumes that it must be instantiated at exactly the same type, which it isn't. With the signature, the type-checker knows that 'fact' is polymorphic and that it's perfectly all right to instantiate it at a different type in the recursive call. Well, at least that's what I worked out from my sparse knowledge, if I'm wrong, would somebody please correct me?

Thanks,

Greg Buchholz

HTH, Daniel

Keean Schupke wrote:

Daniel Fischer wrote:

...

And, BTW, that's why Keean et al's HList library doesn't help here either, the type of an HList determines the number of elements and the type of each, so there we face the same problems as with nested tuples. What we need is type Stack = [ArbitraryType] (from the HList paper, I surmise that [Dynamic] would be possible, but that seems to have it's own problems).

Well it depends on what you want to do... If the types of elements are determined by the computation then you can use an HList as is, and there is no problem.

The problem is that for the recursion combinators we need polymorphic recursion functions. For fact3 we need rec2 :: forall l. (HCons a (HCons a l) -> HCons a l), which is illegal in an HList (at least, I haven't found a way to make it acceptable) and in tuples. For the general recursion combinator it's even worse, because rec2 may take n2 elements of certain types from the stack, does something with them and put k2 elements of certain types determined by the types of the consumed elements on the stack, leaving the remainder of the stack unchanged, rec1 takes n1 elements etc. And the numbers n2, n1 . . . and the types depend on the supplied recursion functions. So (reverting to nested pairs notation), we would have to make linrec to accept arguments for rec2 of the types (a,b) -> (r,b), (a,(a1,b)) -> (r,(r1,(r2,b))), (a,(a1,b)) -> (r,b) (a,(a1,(a2,b))) -> (r,b) and so on, for arbitrary munch- and return-numbers, where we don't care what b is. These can't be unified however, so I think it's impossible to transfer these combinators faithfully to a strongly typed language. [Dynamic] won't work either, I believe, because Dynamic objects must be monomorphic, as I've just read in the doc. The point is, in Joy all these functions would have type Stack -> Stack and we can't make a stack of four elements the same type as a stack of six elements using either nested pairs or HLists (correct me if I'm wrong, you know HList better than I do). However, Joy has only very few datatypes (according to the introduction I looked at), so data Elem = Bool Bool | Char Char | Int Integer | Double Double | String String | Fun (Stack -> Stack) | List [Elem] | Set [Int] type Stack = [Elem] type Joy = State Stack (IO ()) looks implementable, probably a lot to write, but not too difficult - maybe, I'll try.

The only time there is a problem is if the _type_ of an element to be put in an HList depends on an IO action. In this case you need to existentially quantify the HList.

How would I do that? What the user's guide says about existential quantification isn't enough for me.

So you can use the HList in both cases, but you have to deal with existential types if the type of the HList is dependant on IO (you dont have to do this if only the value of an element depends on IO).

Keean.

If you can faithfully implement Greg's code (including fact3-5) using HList, I'd be interested to see it, I think HList suits other purposes far better. Daniel

Am Dienstag, 8. März 2005 17:31 schrieben Sie:

Daniel Fischer wrote:

...

The problem is that for the recursion combinators we need polymorphic recursion functions. For fact3 we need rec2 :: forall l. (HCons a (HCons a l) -> HCons a l),

I dont see why this is illegal... what do we want? take the top two items from the stack?

It's illegal, because a type variable may not be instantiated by a forall-type; section 7.4.9 of the user's guide: There is one place you cannot put a forall: you cannot instantiate a type variable with a forall-type. So you cannot make a forall-type the argument of a type constructor. So these types are illegal: x1 :: [forall a. a->a] x2 :: (forall a. a->a, Int) x3 :: Maybe (forall a. a->a). I'd say that also applys to HList, HCons (forall l. (HCons a (HCons a l) -> HCons a l)) blah won't work (and my ghci doesn't swallow it).

Take the to N elements from the stack:

class Take l n h t | l n -> h t where take :: l -> n -> (h,t) instance Take l HZero HNil l where take l _ = (HNil,l) instance Take t n (h',t') => Take (HCons h t) (HSucc n) (HCons h h',t') where take (HCons h t) (_::HSucc n) = (HCons h h',t') where (h',t') = take t (undefined::n)

Good, but cumbersome. And I'm not sure what the type signature should be for genrec (HCons rec2 (HCons rec1 (HCons t (HCons b stack)))) | hHead (b stack) = t stack | otherwise = rec2 (HCons (genrec.quote rec2.quote rec1.quote t.quote b) (rec1 stack)) I dare say it would be easier in Haskell-style: genrec rec2 rec1 t b stack.

...

For the general recursion combinator it's even worse, because rec2 may take n2 elements of certain types from the stack, does something with them and put k2 elements of certain types determined by the types of the consumed elements on the stack, leaving the remainder of the stack unchanged, rec1 takes n1 elements etc. And the numbers n2, n1 . . . and the types depend on the supplied recursion functions. So (reverting to nested pairs notation), we would have to make linrec to accept arguments for rec2 of the types (a,b) -> (r,b), (a,(a1,b)) -> (r,(r1,(r2,b))), (a,(a1,b)) -> (r,b) (a,(a1,(a2,b))) -> (r,b)

and so on, for arbitrary munch- and return-numbers, where we don't care what b is. These can't be unified however, so I think it's impossible to transfer these combinators faithfully to a strongly typed language. [Dynamic] won't work either, I believe, because Dynamic objects must be monomorphic, as I've just read in the doc.

The point is, in Joy all these functions would have type Stack -> Stack and we can't make a stack of four elements the same type as a stack of six elements using either nested pairs or HLists (correct me if I'm wrong, you know HList better than I do).

They are not the same type, but that are the same Kind, or Type-Familly...

Aye, but as I understand it, once we push the recursion functions on the stack, they must be monomorphic, which means, the scheme won't work in general.

class Stack s instance Stack HNil instance Stack s => Stack (HCons a s)

Isn't this exactly the HList class?

isItAStack :: Stack s => s -> s isItAStack = id

...

However, Joy has only very few datatypes (according to the introduction I looked at), so

data Elem = Bool Bool

| Char Char | Int Integer | Double Double | String String | Fun (Stack -> Stack) | List [Elem] | Set [Int]

type Stack = [Elem]

type Joy = State Stack (IO ())

looks implementable, probably a lot to write, but not too difficult - maybe, I'll try.

The above can be translated to HLists, the difference is that with HLists the types (classes) are extensible.

Might well be, only I don't see how (would have to take a lonnnnnnnng look at HList, probably). Of course, doing it the primitive way means a lot of work every time you add a new datatype :-( But for these types, I did it (with a few modifications) and all works fine.

There appears to be no IO in the example Joy code so existentials are unneccessary.

No IO around, I only thought I might wish to write an interactive frontend, printing out the top of the stack (might be an error message) after each step. I haven't got round to that yet, and I don't know whether I will, but I think if I do, I'd better use type Joy = IO (State Stack Elem).

Keean.

Daniel

Greg Buchholz wrote:

Keean Schupke wrote:

...

I dont see why this is illegal... what do we want? take the top two items from the stack?

With the code below (direct translation from tuples to HLists) I still get an occurs check error when trying to define fact5...

Okay the reason is that types in the code end up depending on values. The type of the stack changes when items are pushed or popped. So the type of the stack returned from recursive functions depends on the recursion count... Haskell is not dependantly typed, so cannot deal with types that "depend" on values. This is why your code with tuples, and the HList code (which is really doing the same thing through a defined API) both fall down on the recursion. One solution is to make all elements the same type and use lists... like: data Elem = ElemInt Int | ElemChar Char... But this looses any static type checking. The alternative is to lift the "values" to the type level, using something like Peano numbers to represent naturals: data HZero = HZero data HSucc x = HSucc x Now different values have explictly different types, so we can have types which depend on them... Attached is an example implementation of "times" using this technique and the HList library (its not debugged... so there might be some mistakes). Keean.

...

...

...

...

Greg Buchholz wrote (on Wed, 09 Mar 2005 at 20:08):

> Can anyone recommend a nice dependently typed language to play with? > Cayenne, Epigram, other? http://www.cs.chalmers.se/~catarina/agda/ See also the sexy IDE alfa: http://www.cs.chalmers.se/~hallgren/Alfa/ Peter Hancock

Keean Schupke wrote:

I have refactored your code into a type level Haskell program. This has the nice advantage that it is extensible.

Wow. Color me impressed. A little under a week ago, I stumbled onto Joy, and thought to myself that it could be translated almost directly into Haskell (which would imply it was possible to statically type). Well, it wasn't quite as direct as I had initially thought, but it looks like you've done it. Are there any papers/books out there which I could study to learn more about these (and other) tricks of the type system wizards? Thanks, Greg Buchholz

Keean Schupke wrote:

The things to notice are using types as instance labels, that constraints form horn clause compile time meta-programs (in a non-backtracking prolog style) and that multi-parameter classes with functional depandencies simulate some dependant types.

I think I understood everything in that sentance up to the word "as" ;-) Greg

On Mon, Mar 07, 2005 at 08:47:11PM +0100, Daniel Fischer wrote:

And, BTW, that's why Keean et al's HList library doesn't help here either, the type of an HList determines the number of elements and the type of each, so there we face the same problems as with nested tuples. What we need is type Stack = [ArbitraryType] (from the HList paper, I surmise that [Dynamic] would be possilble, but that seems to have it's own problems).

It would be interesting if you could use the HList framework for 'partially typed lists' in that if your stack is an hlist, an operation like plus would be plus :: forall a. HList a => Int :*: Int :*: a -> Int :*: a which says that plus goes from ANY Hlist starting with two ints and returns that hlist with a single Int on it. basically you use a universally quantified type to represent the unknown tail of the list (everything else on the stack). not sure if it works.. just brainstorming.... It seems very natural if it could be made to work. John -- John Meacham - ⑆repetae.net⑆john⑈