Slightly more general definition of take

[weaversa]

I came up with a definition of take that allows take`{front=inf} (is it cheating to use zero in this way?)

take : {front, back, a} [front + back]a -> [front]a
take xs = [ x | x <- xs | _ <- zero : [front] ]

This isn't pressing, but I haven't been able to come up with a more general definition of drop that allows drop`{front=inf} [0...] == [].

[msaaltink]

You do not actually need zero for this:

take : {front, back, a} [front + back]a -> [front]a
take xs = xs' where xs' = [ x | x <- xs | _ <- xs' ]

[brianhuffman]

I think a generic drop : {front, back, a} [front + back]a -> [back]a is actually impossible to implement: What would it return when front = inf? So drop has a fin constraint, and then take gets one too because actually neither take nor drop is a primitive; they are both implemented in terms of splitAt, which needs a fin constraint for the same reason drop does.

If we make take and drop into primitives instead of splitAt, then it would be easy to give take a slightly more general type.

[brianhuffman]

Related to generalizing the type of take, we could also generalize the type of append:

(#) : {front, back, a} (fin front) =>
        [front]a -> [back]a -> [front + back]a

The type currently has a fin constraint on the front, which we could get rid of. If front = inf, that means that (#) just ignores its second argument, which is a bit weird, but it would work. And it's probably nice to keep the types of take and (#) consistent with each other.

[robdockins]

I've wondered before about relaxing the type of take. I think it probably makes sense to do that, and I agree that the right way to go about it is to make take and drop primitives. If we relax the type of (#), however, it would be kind of strange because then # in pattern-match position (which is desugared into splitAt) would not match # in value position.

[yav]

I mean, we could just drop the fin constraint from splitAt and make things work. For example, when you split at inf you'd end up with ([inf] a, [n] b) because inf + n = inf.

I am skeptical of these generalizations though, as I think of arrays and streams as being rather different, and I think the current type nicely express the interaction between the two. To me taking or dropping inf many things seems more likely to be an error, so I'd rather leave the types as they are. If someone needs the more general version of take, then they can define it as shown above.

[robdockins]

And then you get, what, undefined : [n]a as the second output? I don't love that.

[weaversa]

I was thinking you’d get []. The type defaulting engine will choose n=0, right?

[robdockins]

And one reason to consider making take a primitive is that it is essentially a no-op in the interpreter, whereas it sets up memo tables and causes a lot of allocations if you make it a comprehension.

[robdockins]

You'd only get [] when n = 0

[weaversa]

Won’t the type system default n to 0?

[robdockins]

Yes, but you could make it take on any value by giving a signature

[yav]

No matter how long the second part is, its value would be undefined. That's that value that is at the end of an infinitely long list :)

[brianhuffman]

The more general type of take would be nice for letting us define a more generic form of generate, which could work also for infinite lists.

[brianhuffman]

If we really want to have infinitely long lists with values "at the end", we can just redefine kind # from extended natural numbers to countable ordinals. Then we can have 1+inf = inf, but inf+1 > inf, and a type like [inf+1]a would have infinitely many as followed by one more at the end. You could use splitAt`{inf,1} to take it apart. We could also use join on something of type [inf][inf]a to get a super-long list of type [inf*inf]a, which we could then split apart again to get the original value. The only drawback is that it would make typechecking a bit harder, as we'd have to teach z3 to do ordinal arithmetic ;)

[robdockins]

Has anybody tried to design a language with ordinal array indexing? Seems like an interesting challenge...

[msaaltink]

I think that the idea was to have front = inf imply back=0, which makes a sort of sense. It is I think possible to code that up in a type signature

drop : {front, back, a} ( (min 1 back)*(front+1) + (1-(min 1 back)) != (min 1 back)*front) =>  [front+back]a -> [back]a

[robdockins]

The type of take was generalized via d3accfb