Re: Types for Perl 6: request for comments
On 24/06/15 21:27, yary wrote:
I'm reading it a bit at a time on lunch break, thanks for sending it
along, it's educational.
My comments here are all about the example on the top of page 5,
starting with the minutest. First a typo, it says subC where it
should say sumC
multi sub sumB is ambiguous, due to your use of ;; there. And sumI
/should/ be ambiguous, because the caller sumC(Int $x ;; $y)
{sumI($x,$y)} means sumI will always be called with $x - Int and
varying $y. That example could use a little re-working.
Oh, right, Thank you, I apologize, I did some cutpaste errors in this
code (I run all the code on rakudo but I must have missed this one).
Here you are the correct version. I updated the paper online
multi sub sumI(Int $y ;; Int $x){ $x + $y }
multi sub sumI(Bool $y ;; Int $x) { sumC($y,$x)}
multi sub sumB(Bool $y ;; Bool $x) { $x $y }
multi sub sumB(Int $y ;; Bool $x) { sumC($x,$y0) }
multi sub sumC(Int $x ;; Int|Bool $y) { sumI($y,$x) }
multi sub sumC(Bool $x ;; Int|Bool $y) { sumB($y,$x) }
I also added an explaination ... now it should be clearer.
Note to Rakudo-porters: Can the error message remember the ;; in
the sig ? The message from Rakudo * has a , where the source has
;; which is misleading:
Ambiguous call to 'sumB'; these signatures all match:
:(Bool $y, Bool $x)
:(Bool $y, Int $x)
The comment example about considering anonymous multi definitions
in the same block to define the same anonymous function does show the
feature's desirability, but that proposed syntax might be problematic.
(Deciding if how to make that part of the syntax is not in the scope
of the paper, but since you brought it up) What if one wants to
define two different anonymous multi subs in the same scope? A
contrived example:
sub pick_multi (Bool $p) {
my multi sub hmmI(Int $y) { 2 * $y }
my multi sub hmmI(Bool $y) { $y }
my multi sub hmmB(Int $y) { 1 + $y }
my multi sub hmmB(Bool $y) { ! $y }
$p ?? hmmI !! hmmB
}
Yes, one could enclose each anon-multi-set in a do block, but it
feels to me that defining an anonymous multi-sub should require a
single statement, to avoid unintentional co-mingling within a block.
I see, but my purpose was completely different. I did not want define
local multi-subroutines, I want to define a function whose *result* is a
multi subroutine.
So the intended meaning of
multi sub sumC(Int $x){
multi sub (Int $y) { $x + $y }
multi sub (Bool $y) { sumC ($y)($x) }
}
is
multi sub sumC(Int $x){
return {
multi sub (Int $y) { $x + $y }
multi sub (Bool $y) { sumC ($y)($x) }
}
}
in the same way as
multi sub sumC(Int $x){ sub (Int $y){$x + $y } }
stands for
multi sub sumC(Int $x){ return {sub (Int $y){$x + $y }} }
Again I added some more explaination in the text.
Now that I've thought about it for 90 seconds (not fully-formed idea),
if one were to have an anonymous multi-sub, it ought to be constructed
from a list of /signature/, /body /pairs.
And/or, any non-finalized sub could have a method to add another
/signature, body/ to its dispatch list.
Yes, or just as I proposed the list is the argument of the return. I
think that the notation I proposed in the paper should not pose any
problem to the parser (or the programmer). But as you said, I am out of
topic here at least as long as this paper is concerned.
my $sub = do {
proto foo (|) { * }
multi foo (Int $x) { $x + 1 }
multi foo (Str $y) { $y ~ 'a' }
foo;
}
Oh yes, nice ... I think I will add it in my paper (and if you send me
your full name I will give credits to you)
Thanks a lot, this is the kind of feedback I really was looking for.
--Beppe---
Types for Perl 6: request for comments
I wrote an article trying explain/propose (static) typing for Perl 6. In particular I explain how to type subs, multi subs, classes, multi methods; how to use union, intersection and subset types; and I finally use these notions to explain the old problem of covariance vs. contravariance in object-oriented programming. The target reader of (the first part of) the article is every Perl 6 programmer, which is why all the above is explained by examples of Perl 6 code (no formula, theory, theorem, or property whatsoever) and I tried to do my best to make the article completely self-contained. This is also why comments from this mailing list are *very* welcome. The second part of the paper targets language implementers and designers: if the first part convinced you of the usefulness of such (possibly optional) types, then you will find in the second part the details of data structures and algorithms to efficiently implement this type system. I also give extensive references in which you will find how to extend the system by some missing bits (notably, polymorphism). The paper can be retrieved at the following url. http://www.pps.univ-paris-diderot.fr/~gc/papers/perl6-typing.pdf I insist, comments from Perl 6 programmers will be extremely welcome: just do not be (too) harsh, please :-) Thank you in advance for your help Giuseppe Castagna
Re: question - languages with set/foo as only base data type
There is a programming language in which types are sets (of values) and that is designed all on this interpretation (even though integer values are primitive and not encoded as you suggest). The language is CDuce where, besides basic function and product types, you have also (set-theoretic) union, intersection and negation type connectives. You can try it here http://www.cduce.org. It is also included in all major linux distributions. If you are more interested at the theory rather than the implementation, then I suggest to start with the paper A gentle introduction on semantic subtyping and then move to the reference paper Semantic subtyping published in the Journal of the ACM. Polymorphism is then done in a ICFP 2011 paper and in a forthcoming POPL 2014 paper. The type system nicely fits Perl6 (really nicely!). I am currently writing a primer on how adapt these types and they algorithms and data structures to Perl6 ... but do not hold your breath. If you are interested please do not hesitate to ask more information. Beppe P.S. For what concerns homotopy type theory, it tries to overcome some limitation of set-theory, that is, if I understood correctly just the contrary of what you intend to do On 18/11/13 00:33, raiph mellor wrote: On Sun, Nov 17, 2013 at 5:43 PM, Andrew Suffield asuffi...@suffields.me.uk mailto:asuffi...@suffields.me.uk wrote: While mathematics as a field has mostly settled on set theory as its basis, type theory is equally expressive and is usually preferred in language design. Aiui there is now optimism in some circles that the set theory foundation will be replaced by a homotopical interpretation of type theory. I have about zero understanding of what this stuff is or if it will have any impact on programming language type systems, but thought I'd speak up. :) -- raiph
Re: Are set operations needed?
On 18/07/13 17:58, Patrick R. Michaud wrote: [...] Sets do not implement well on a computer. Let me strongly disagree with this statement. Sets implement *very well* on computer, it just suffices to know how to do it. You want a constructive proof? Check the CDuce language (http://www.cduce.org) where types are sets of values, you have all the set-theoretic operations listed in a previous mail, pattern matching is based on type-case (that is dynamic testing the type of the matched value), you have dynamic overloading as you do in Perl6. As added bonus, the language is statically type-safe and you can also have polymorphic functions (not implemented yet, but should be available in an year or so). ... and efficiency is not an issue. My two cents' worth Beppe
Re: Type system for Perl 6
Thank you very much for your answers. As I said in my post I knew the synopsis,
but I hoped to have something more precise. I will explore it again by using
Timoty roadmap
On 02/05/2010 01:59 AM, Darren Duncan wrote:
G. Castagna: Covariance and contravariance: conflict without a cause. ACM
Transactions on Programming Languages and Systems, vol. 17, n. 3, pag.
431-447, 1995.
Is there an electronic copy of this that you can link to?
Ah, spoke too soon. An electronic copy is linked to from one of the other
sites you gave, at http://www.pps.jussieu.fr/~gc/selected.en.html ; the PDF
version is at http://www.pps.jussieu.fr/~gc/papers/toplas95.pdf .
Well, glad you found the contravariance paper. For what concerns CDuce, the
language is included in most linux distributions (Ubuntu Debian, Fedora,
Mandriva, at least). For the type system, while I think that the
contravariance paper is rather accessible (I hope), the most accessible
presentation for CDuce types is probably the joint keynote talk I gave at PPDP
and ICALP, that can retrieved here
http://www.pps.jussieu.fr/~gc/papers/icalp-ppdp05.pdf
while it is a little bit technical, you can use the covariance paper as a key of
reading: the type of an overloaded function (set of arrows) is there an
intersection of the arrows.
And by union types, I mean both that you can say Dog | Cat (syntax?) to
allow either Dog or Cat values, and also that Perl 6 roles effectively
declare union types but that the members add themselves to the union rather
than the union itself declaring what it ranges over; in the latter case, the
union type is every value that does this role.
Well union for must are just ... unions. So the type Int | Bool | Dog is
intuitively the set {Dog, true, false, 1, 2, 3, }. That is, both
enmuerated sets, and set theoretic unions.
Finally, if you use the CDuce type theory for Perl 6 you obtain for free pattern
matching for XML values, if you are interested in it (probably it will require a
little effort to make the syntax compatible with perl regexps).
I see I'm going out of the scope of this list. I apologize for spamming, but
please continue to post here or send me by PM every information about Perls 6 types.
---Beppe---
Re: Type system for Perl 6
On 02/05/2010 10:53 PM, TSa (Thomas Sandlaß) wrote: HaloO Mr Castagna I'm delighted to have you interested in Perl 6. I know your book and articles and have argued for a type system of Perl 6 here on the list for quite a while. Wow, so actually somebody read it! :-) Thank you Unfortunately I'm not able to implement one for Parrot or so. But if you are willing to port the CDuce code this is a great thing! Well, I really have not time nor human power to do it, but the specification is pretty simple for anyone with a functional language background. I can provide more information if needed. As a matter of fact I am going to define it in the work that is at the origin of my first post, so stay tuned. and all objects that do A are also B doers. So one could infer that we have A: B. But note that this subtype relation is not enforced in the body of the role or in the class it is composed into. Yes I saw that inheritance is not subtyping. I would not share this decision since as an outsider, it seems to me that Perl6 has redundant syntax (too many different ways to express the same thing), so it is astonishing that in that case the choice was to use the same keywork for two different things. But it is likely that I missed the point there. The spec says nothing about class inheritance and type narrowness. Parametric roles are covariant on their type parameter irrespective of its use. Yeah I also noticed that reading the Parametric subtyping section in Chapter 14 of the Synopsis. This is quite unfortunate since the right way to deal with all these issues has been well known for at least ten years (e.g. Bounded and F-bounded polymorphism and variance annotations), even though it is just recently that they appeared in maistream languages (e.g. variance annotations in C# 4.0). Actually I noticed an old post you did on this list 5 years ago. It contained the following drawing A|B lub (lowest upper bound) / \ / \ A 0 B / \ / \ / \ / \ / AB \ glb (greatest lower bound) / 1 / \ 2 \ / / 3 \ \ and it is the only reference I found to intersection types (since AB is the intersection of A and B (if you consider a class type as the set of all its instances) that is it contains all objects that are instance both of A and of B. Is this notation (or the general idea of intersection types) has been abandoned since then (I was not able to find it in the synopsis) Cheers Beppe
Re: Type system for Perl 6
On 02/05/2010 11:29 PM, Jonathan Worthington wrote: And the odering in dispatch is not a type lattice as in Cecil but a topological ordering. Again I've no clue what that means. and all objects that do A are also B doers. So one could infer that we have A : B. But note that this subtype relation is not enforced in the body of the role or in the class it is composed into. Can you clarify what you mean by not enforced? I interpreted Thomas remark as the fact tha declaring subclass does not enforce safe substiatability. Am I wrong? Parametric roles are covariant on their type parameter irrespective of its use. E.g. you can declare a read/write attribute of that type. While parametric roles do fill the niche of parametric types, you can also parametrize them with values - STD (the standard grammar) takes advantage of this. In many ways, a parametric role definition works like a kind of role factory; an implementation falls quite naturally out of multiple dispatch and closure semantics. Seeing parametric roles as being solely for parametric polymorphism is casting their role in Perl 6 a little too narrowly though. I think nobody wanted to do it. The point is that if you add variance annontation (as in C# or Scala) to specify where you can use the type parameters coavariantly or contravariantly give you the same flexibility and furthermore type safety. The PL researcher I know at Javasoft still regret to have allowed covariance for Arrays (this is just second in the regret list, the first being that production people did not allow them to change the JVM to deal with generics in the bytecode). I agree that the information that is available on the Perl 6 type system is scattered across the synopses, and in some places probably needs a look at the spectests, and probably has untested edge-cases too. Maybe it'd be good to try and collect it together more at some point, so there's a single source to point people at. This is exactly my problem. I decided to post here after spending a couple of days just trying to understand what the precise syntax of types is in Perl6. Hope this helps, Yes. Actually the best source of information on types I found is your FAQ, that I was reading when I received your mail. Centralizing the information there would be much useful ... at least for me. Thank you for both. Beppe
Re: Type system for Perl 6
On 02/05/2010 11:54 PM, Jonathan Worthington wrote: If you want to check if A inherits from B, do A.isa(B). If you want to check if A does B, do A.does(B). If you just care if A is somehow a subtype of B, but don't care why, do A ~~ B. Much of the time, the last of these is the important one. This is great information. The kind of information that I am sure can be found in the Synopsis, but not so clearly explained and summarized in just one point. I will start experimenting with it. Thanks *a lot* ---Beppe---
Type system for Perl 6
Hi, I would like to know where I can find the latest documentation on the type (and above all subtype) system for Perl 6. The synopsis does not say much about it. I found this: http://www.dlugosz.com/Perl6/web/typesystem-summary.html but agin there is not much information. If your are curious about my interest, the reason is that I wanted to propose a type system for a core of Perl 6. The idea is to use the type system of the CDuce language (http://www.cduce.org) without the XML part but using the same technique used there to type the (late bound) overloaded functions (akin to multi-methods). I want to adapt it to Perl 6 multi sub/methods (with ;; parameters) by using the ideas I wrote long ago in the following paper: G. Castagna: Covariance and contravariance: conflict without a cause. ACM Transactions on Programming Languages and Systems, vol. 17, n. 3, pag. 431-447, 1995. the advantage is that combining these old ideas with the recent advances of the Cduce type system should yield a type system very easy to understand and use for the average programmer since it relies on simple notions such as union, intersection, and set (of values) containment. Furthermore the powerful (sub-)typing algorithms developed CDuce could be probably reused with minor modifications. I would like to know the current status of the Perl6 in order to adapt my presentation. In particular, a complete syntax for types would be welcome (the most complete description I found is this one http://www.programmersheaven.com/2/Perl6-FAQ-Types). Thanks in advance for your help. Of course I will be happy to discuss the details of my proposal on this list, if there is any interest, of course. ---Beppe--- P.S. If you are interested to see what I work on, please check my web page: http://www.pps.jussieu.fr/~gc
