These are chat archives for got-lambda/expression

9th
Dec 2017
Jean-Louis Giordano
@Jell
Dec 09 2017 00:21
I... might have gone a bit berserk on Idris today https://github.com/Jell/advent_of_code_2017/blob/master/idris/Day7.idr
jolod
@jolod
Dec 09 2017 10:24
@Jell Now that you have played with some "real" programs (i.e. read input and print output), do you think that Idris is "worth it"?
Jean-Louis Giordano
@Jell
Dec 09 2017 10:37
as in, can I imagine it evolving towards something I can use in production someday?
jolod
@jolod
Dec 09 2017 10:40
And/or would you ever choose a deptyped language over a Haskell-styled typed language?
For any project that you would do (private or through work).
I don't count puzzles as projects, btw.
Jean-Louis Giordano
@Jell
Dec 09 2017 10:41
I really like idris, and you can do ad-hoc polymorphism without type classes using namespaces, everything is printable at the REPL, and you have the same language at the type-level as at the value-level, making working with types more intuitive
if Idris had the same amounts of libraries as Haskell I'm pretty sure I would use Idris
jolod
@jolod
Dec 09 2017 10:41
OK. Nice.
So you're going even more towards the extremes. Clojure on one end and Idris on the other. And that makes sense.
Jean-Louis Giordano
@Jell
Dec 09 2017 10:42
and the fact the the language unifies types and value makes the REPL experience really good
yes I would say currently my two favourite langs are Clojure and Idris
Haskell I just find myself learning "more types"
which I don't find super interesting
(if that makes sense?)
jolod
@jolod
Dec 09 2017 10:43
What about the fast feedback that compilation gives you? In Idris, you compromise on that, I presume.
Jean-Louis Giordano
@Jell
Dec 09 2017 10:43
I work a lot at the REPL
jolod
@jolod
Dec 09 2017 10:44
Will that approach scale?
Jean-Louis Giordano
@Jell
Dec 09 2017 10:44
you lose the fast feedback if you to too much at compile time
Idris has an incremental compiler though as I understand it, so you can isolate your compile-time shenaningans to a separate module
jolod
@jolod
Dec 09 2017 10:45
So it's manageable by you not writing crazy types?
Jean-Louis Giordano
@Jell
Dec 09 2017 10:45
yeah, pretty much like in Haskell I would say
jolod
@jolod
Dec 09 2017 10:45
Like proving primeness. :-)
Jean-Louis Giordano
@Jell
Dec 09 2017 10:46
my intuition is that given enough maturity, it will be very much useable
still really rough: using TypeProvider segfaults on my machine if I provide anything that's not a String
and I could not compile Day5 with the full input using TypeProviders
Day7 work out fine though
(kinda proud of that one, took me like 5h to solve but if I return a tree in Part 2 I have proven it's balanced, which is pretty cool)
Jean-Louis Giordano
@Jell
Dec 09 2017 10:51
but yeah I really feel that Clojure <-> Idris are currently at the two most extreme of the Spectrum, and weirdly enough I get the same kind of feeling for both
jolod
@jolod
Dec 09 2017 10:52
I haven't read the code. How do you take an unbalanced tree (as the input) and make it balanced? Do you update the odd branch so that it is balanced, and remember that value?
Jean-Louis Giordano
@Jell
Dec 09 2017 10:52
I think it's the consistency (everything is a Value vs everything is a Type maybe?) + REPL experience + First class everything
the type of the Tree is here:
data Tree : (weightSum : Nat) -> Type where
  Leaf : (name : String) -> (weight : Nat) -> (Tree weight)

  Node : (name : String)
      -> (weight : Nat)
      -> (ds : Vect n (Tree subWeight))
      -> (Tree (weight + (n * subWeight)))
so you cannot build a tree that's not balanced
it's not representable
jolod
@jolod
Dec 09 2017 10:53
Personally I don't use the REPL as it's usually implemented, i.e. command line interface. In Python I use a notebook, and in Clojure I use Atom (which uses nREPL of course).
@Jell Right. So how does it work to represent the unbalanced tree?
Jean-Louis Giordano
@Jell
Dec 09 2017 10:54
and so I build up the tree from a List of inputs
makeTree : (inputs   : List (String, Nat, (n ** Vect n String)))
        -> (tmpTrees : List (m ** Tree m))
        -> Either (String, (List (String, Nat, Nat)))
                  (l ** Tree l)
makeTree [] [] = Left ("Can't build tree from empty list", [])
makeTree [] (tree :: others) = Right tree
makeTree ((name, weight, (n ** children)) :: xs) ts =
  if n == 0
  then makeTree xs ((weight ** (Leaf name weight)) :: ts)
  else case findChildren children ts of
            Nothing => Left ("Not in deps order", [])
            (Just cs) => case unifyChildren cs of
                              Nothing => Left ("Not balanced", map infoPaired (toList cs))
(Just r) => makeTree xs ((makeNode name weight r) :: ts)
jolod
@jolod
Dec 09 2017 10:54
@Jell I assume you don't, and that is why when you construct it you need to correct it. Right?
Jean-Louis Giordano
@Jell
Dec 09 2017 10:54
yes correct @jolod
jolod
@jolod
Dec 09 2017 10:55
So you can also be fairly sure that the returned correction is correct.
Jean-Louis Giordano
@Jell
Dec 09 2017 10:55
I have an intermediate "list of subtrees"
yeah I'm sure off it because I fix it, recompile and get a balanced tree, with the top root being the one I expected
jolod
@jolod
Dec 09 2017 10:56
Wait what?
recompile?
Jean-Louis Giordano
@Jell
Dec 09 2017 10:56
yeah because I read the input at compile time :p
makes my life easier and you get a bunch of proof statically
at the repl it's just reload
jolod
@jolod
Dec 09 2017 10:57
But what if you wrote this as a server, and you get input through a request and you need to reply with the offending disc and how much it is off?
Jean-Louis Giordano
@Jell
Dec 09 2017 10:58
it's fine it's just I have to add a bit more boiler plate
jolod
@jolod
Dec 09 2017 10:58
But you read the input at compile time?
Jean-Louis Giordano
@Jell
Dec 09 2017 10:58
you need to parametrise more stuff with dependent pairs
jolod
@jolod
Dec 09 2017 10:58
Are compile and run-time intertwined?
Jean-Louis Giordano
@Jell
Dec 09 2017 10:59
I don't think I understand dependent types well enough to explain what's going on
but the "dependent" part of dependent types is that you can have a type depend on a runtime value
so if you look at this line:
jolod
@jolod
Dec 09 2017 11:00
Yeah. But do you need to read the input at compile time?
Jean-Louis Giordano
@Jell
Dec 09 2017 11:00
parseLine : String -> Maybe (String, Nat, (n ** Vect n String))
jolod
@jolod
Dec 09 2017 11:01
What is **?
Jean-Louis Giordano
@Jell
Dec 09 2017 11:01
that's a dependent pair
jolod
@jolod
Dec 09 2017 11:01
OK.
Jean-Louis Giordano
@Jell
Dec 09 2017 11:01
it means "this is a type that depends on a runtime value", which is the first part of the type
jolod
@jolod
Dec 09 2017 11:01
Well, before we go too deep, maybe I should just learn Idris. :-)
That'll be the language of 2018 then I guess.
Jean-Louis Giordano
@Jell
Dec 09 2017 11:02
it's really cool, the book is awesome
oh one thing you lose in Idris is top-level type inference of course
but you get code inference instead so ¯\_(ツ)_/¯
jolod
@jolod
Dec 09 2017 11:05
;-P
Jean-Louis Giordano
@Jell
Dec 09 2017 11:32
geez can't let it go, now I've fixed the type so a Node has at least one children (otherwise there was ambibuity between the constructors Leaf "foo" 10 and Node "foo" 10 [])
data Tree : (weightSum : Nat) -> Type where
  Leaf : (name : String) -> (weight : Nat) -> (Tree weight)

  Node : (name : String)
      -> (weight : Nat)
      -> (ds : Vect (S n) (Tree subWeight))
      -> (Tree (weight + ((S n) * subWeight)))
which, come to think of it, perhaps I only need one constructure
Jean-Louis Giordano
@Jell
Dec 09 2017 11:39
ah! fun fact: that would not be so elegant because then one needs to pick an arbitrary subWeight for leaf nodes!
ok I'm off, sorry for the noise I get carried away as usual
:wave:
Erik Svedäng
@eriksvedang
Dec 09 2017 12:10
Very interesting!
Jean-Louis Giordano
@Jell
Dec 09 2017 16:53
my Idris status update: my Day 7 solution is now proven to be total! \o/
the interesting bit is here:
-- Dependency solver
depsOrder : (xs  : List (String, Nat, (n ** Vect n String)))
         -> (tmp : List (String, Nat, (n ** Vect n String)))
         -- Add bound retries for totality check
         -> {default (fact (length xs)) retries : Nat}
         -> Maybe (List (String, Nat, (n ** Vect n String)))
depsOrder [] deps = Just $ reverse deps
depsOrder {retries=(S rets)} ((name, weight, (n ** children)) :: xs) deps =
  if n == 0 || all (\c => elem c (map fst deps)) children
  then depsOrder {retries=rets} xs ((name, weight, (n ** children)) :: deps)
  else depsOrder {retries=rets} (xs ++ [(name, weight, (n ** children))]) deps
depsOrder _ _ = Nothing
the default ... retries avoids infinite recursion by bounding the algorithm with O(n!)
I thought it was a neat trick
which turned the above function from a partial function to a total function returning a Maybe
Jean-Louis Giordano
@Jell
Dec 09 2017 18:03
saw Day 9 and I immediately thought: this is the perfect use for a parser combinator! So I solved it using Regexp instead. :trollface:
Jean-Louis Giordano
@Jell
Dec 09 2017 18:08
(just to be clear: I only solved part 2 only using regexp, and I'm cheating on part 1)
jolod
@jolod
Dec 09 2017 20:24
@Jell :+1: :smile:
jolod
@jolod
Dec 09 2017 23:29
@Jell So I accepted your challenge, and did it in Perl 5.10 using only s///g, while, or, and scalar. Plus $_ = <>;for reading input and say for printing the answer.
Part 1, that is.
Jean-Louis Giordano
@Jell
Dec 09 2017 23:30
:rocket:
jolod
@jolod
Dec 09 2017 23:30
It's not exactly "efficient".
Jean-Louis Giordano
@Jell
Dec 09 2017 23:30
I kinda want to see, on the other hand I know 100% I will not understand any of it :p
jolod
@jolod
Dec 09 2017 23:30
Yeah.
Jean-Louis Giordano
@Jell
Dec 09 2017 23:31
I don't think sharing would be considered a spoiler :p
jolod
@jolod
Dec 09 2017 23:31
I'm not even using crazy Perl special forms though.
In the REs I mean.
Here goes:
$_ = <>;
s/,?<(?:!.|[^>])*>,?//g; # Remove garbage.
s/\},?/},/g;
s/\{\}/x/g;
1 while s/\{(x+),\}/x,x$1/g
     or s/\{(x+),([^{} ]+)\}/{$2 x$1,}/g
     or s/\{(x+),([^{} ]+) /{$2 x$1,/g
     or s/\{(x+), ([^{}]*)\}/$2${1}x,x/g;
print scalar s/x/x/g;
Oh, I forgot I added a comment even!
See, it makes sense now!
j/k.
Jean-Louis Giordano
@Jell
Dec 09 2017 23:32
nice! production quality
jolod
@jolod
Dec 09 2017 23:32
It's just a couple of reduction rules.
Jean-Louis Giordano
@Jell
Dec 09 2017 23:35
ah! I see how it works! :)
jolod
@jolod
Dec 09 2017 23:35
Seriously?
Jean-Louis Giordano
@Jell
Dec 09 2017 23:35
you slowly replace all the groups with x?
then you count them?
jolod
@jolod
Dec 09 2017 23:35
Yeah, but not only that.
I need to handle {x,x,}.
Jean-Louis Giordano
@Jell
Dec 09 2017 23:36
yeah that's what the while is in there right? :p
I just hand wave the big chunk in the middle
jolod
@jolod
Dec 09 2017 23:36
That's the tricky part.
Jean-Louis Giordano
@Jell
Dec 09 2017 23:36
$1 are previous captures right?
jolod
@jolod
Dec 09 2017 23:36
{x,x,} should somehow become xx,xx,x
I just realized a different way of doing it that might be easier.
So what I do is that I rewrite {x,x,} to {x, xx,} (notice the space).
And then {x, xx,} to { xx,xx}.
Jean-Louis Giordano
@Jell
Dec 09 2017 23:38
lol
jolod
@jolod
Dec 09 2017 23:38
And then { xx,xx} to x,xx,xx
Do I'm "looping" by circling it and adding and end marker. (The space)
You'd want to do something like (,(x+))+ and somehow remember all the times the inner parenthesis captures, but you only get the last.
You can do it in Perl, but that would involve Perl special-stuff, and that was not what I was going for.
I didn't want a Perl solution. I wanted a reduction system using regexes.
Jean-Louis Giordano
@Jell
Dec 09 2017 23:41
:heart:
jolod
@jolod
Dec 09 2017 23:41
There's not even a lookbehind in there.
jolod
@jolod
Dec 09 2017 23:56
@Jell I reverted a minor optimization so that the output matches how the examples are illustrated.
({{{},{},{{}}}} => x,xx,xxx,xxx,xxx,xxxx,)
Optimization as in substituting less characters in an s///.
Jean-Louis Giordano
@Jell
Dec 09 2017 23:57
kewl