Perl 6 - the future is here, just unevenly distributed

IRC log for #6macros, 2015-10-07

| Channels | #6macros index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
06:34 Ven joined #6macros
06:50 FROGGS joined #6macros
07:03 Ven o/
07:35 masak \o
07:35 masak I found it tough going to just translate the Vector example straight into something Perl 6-like.
07:52 Ven yeah
07:52 Ven ENO[G]ADT
07:52 Ven have to resort to inheritance => is now runtime
07:58 masak it wasn't just that.
07:58 masak I felt I understand what the Idris version does, but it's such a different view of the world from how I would write a Perl 6 class or role, say.
07:58 masak the Idris version feels more like a Haskell typeclass or something.
07:59 Ven not sure why it feels like a typeclass to you
07:59 Ven those would be more like, er, interfaces
08:03 masak I'm having trouble verbalizing this, but let me try -- I think it's important for my understanding, too
08:04 masak ok, so
08:04 masak data Vect : Nat -> Type -> Type where
08:04 masak this line says that a Vect is a type, that you construct by giving it a Nat and a type
08:05 masak the two subsequent lines are indented, and talk about two other global names related to Vect
08:05 masak Nil  : Vect Z a
08:06 masak this is a constant, basically creating an instance of the new type we just defined
08:06 masak I'm a wee bit surprised that one can use `a` like that -- it hasn't been bound anywhere
08:07 Ven ImplicitForAlls, like in haskell
08:07 masak I guess there's some convention there going on that I'm unaware of -- something like "a single-letter lower-case variable is a type capture" or whatever
08:07 Ven (but unlike agda)
08:07 masak right
08:07 masak my sense of such things is still weak
08:08 masak finally
08:08 masak (::) : a -> Vect k a -> Vect (S k) a
08:08 masak means there's an infix :: operator which takes an element and a vector, and creates a new vector with the new element
08:09 masak only now does it become clear to me that all of these definitions are talking about the signatures completely on the type level
08:09 masak if there's such a thing as "completely on the type level" in Idris
08:12 masak does that mean that... Nil is a type? it kinda has to be, right? since it contains an `a` implicitforall thing
08:18 Ven Nil is a type ctor
08:19 Ven if you're not used to GADTs in Haskell, it can be confusing
08:19 Ven (::) : a -> Vect k a -> Vect (S k) a=>that means
08:19 Ven ":: has two fields: a and Vect k a"
08:19 Ven and its type (in Vect) is Vect (S k) a
08:39 Ven ["APL", "Assembly", "C", "LiveScript", "Perl6", "Clojure", "JavaScript", "Perl", "CoffeeScript", "Awk", "C++", "COBOL", "Agda", "Racket", "Emacs", "PHP", "Scala", "Swift", "F#", "HTML", "Objective-C", "Elixir", "Common", "Java", "D", "Erlang", "Ruby", "Tcl"]
08:39 Ven That's my list of "github languages".
08:58 Ven joined #6macros
10:08 Ven joined #6macros
10:59 Ven joined #6macros
11:08 Ven_ joined #6macros
11:18 masak ok, they're both type ctors. got it.
11:19 masak and I guess you get a lot of things for free with those. for example, they end up being the cases you need to cover in a pattern matching on that type.
11:21 cgfbee joined #6macros
12:31 Ven_ joined #6macros
14:14 FROGGS joined #6macros
14:44 Ven_ joined #6macros
17:23 FROGGS joined #6macros
20:05 * vendethiel reads the 007 commit
20:05 vendethiel err, commits* :-)
20:07 vendethiel I always forget and proceed...
20:26 masak I put in the `proceed` there because I didn't want to duplicate the `die`

| Channels | #6macros index | Today | | Search | Google Search | Plain-Text | summary