|
6macros: discussing the finer points of Perl 6 macros, Qtrees, and how to stay sane | irclog: irclog.perlgeek.de/6macros/today Set by moderator on 28 July 2015. |
|||
|
06:34
Ven joined
06:50
FROGGS joined
|
|||
| Ven | o/ | 07:03 | |
| masak | \\o | 07:35 | |
| I found it tough going to just translate the Vector example straight into something Perl 6-like. | |||
| Ven | yeah | 07:52 | |
| ENO[G]ADT | |||
| have to resort to inheritance => is now runtime | |||
| masak | it wasn't just that. | 07:58 | |
| 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. | |||
| the Idris version feels more like a Haskell typeclass or something. | |||
| Ven | not sure why it feels like a typeclass to you | 07:59 | |
| those would be more like, er, interfaces | |||
| masak | I'm having trouble verbalizing this, but let me try -- I think it's important for my understanding, too | 08:03 | |
| ok, so | 08:04 | ||
| data Vect : Nat -> Type -> Type where | |||
| this line says that a Vect is a type, that you construct by giving it a Nat and a type | |||
| the two subsequent lines are indented, and talk about two other global names related to Vect | 08:05 | ||
| Nil : Vect Z a | |||
| this is a constant, basically creating an instance of the new type we just defined | 08:06 | ||
| I'm a wee bit surprised that one can use `a` like that -- it hasn't been bound anywhere | |||
| 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 | ||
| Ven | (but unlike agda) | ||
| masak | right | ||
| my sense of such things is still weak | |||
| finally | 08:08 | ||
| (::) : a -> Vect k a -> Vect (S k) a | |||
| means there's an infix :: operator which takes an element and a vector, and creates a new vector with the new element | |||
| 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 | ||
| if there's such a thing as "completely on the type level" in Idris | |||
| does that mean that... Nil is a type? it kinda has to be, right? since it contains an `a` implicitforall thing | 08:12 | ||
| Ven | Nil is a type ctor | 08:18 | |
| if you're not used to GADTs in Haskell, it can be confusing | 08:19 | ||
| (::) : a -> Vect k a -> Vect (S k) a=>that means | |||
| ":: has two fields: a and Vect k a" | |||
| and its type (in Vect) is Vect (S k) a | |||
| ["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 | ||
| That's my list of "github languages". | |||
|
08:58
Ven joined
10:08
Ven joined
10:59
Ven joined
11:08
Ven_ joined
|
|||
| masak | ok, they're both type ctors. got it. | 11:18 | |
| 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:19 | ||
|
11:21
cgfbee joined
12:31
Ven_ joined
14:14
FROGGS joined
14:44
Ven_ joined
17:23
FROGGS joined
|
|||
| vendethiel reads the 007 commit | 20:05 | ||
| err, commits* :-) | |||
| I always forget and proceed... | 20:07 | ||
| masak | I put in the `proceed` there because I didn't want to duplicate the `die` | 20:26 | |