These are chat archives for got-lambda/expression

Dec 2018
Jean-Louis Giordano
Dec 07 2018 12:54
had a little bit of fun with a colleague at lunch break today with basic compile-time unit tests in Idris using type providers:
Pierre Krafft
Dec 07 2018 13:52
@Jell how does it work?
I suppose it works as long as both sides are normalized to the same value?
Jean-Louis Giordano
Dec 07 2018 14:06
yeah it works! it's actually just passing a list of pairs with (Bool, String), if True then nothing happens, if False then fail to provide a type
oh sorry "how does it work" instead of "does it work" :p
so TypeProviders take a value and return a type but does that through an IO monad
so you can basically do type-level IO
in that case you can print the result of the tests and/or fail compilation
there's probably an easier way to do that without involving IO at all, as long as you find a way to fail compilation
but I thought it was cool to do it that way :p
type providers is a really cool concept :p
(they exist in F# as well I believe)
the common use case is to read a schema file or something to generate a type from that
Jean-Louis Giordano
Dec 07 2018 14:57
ah! the Haskell version of type providers?
Dec 07 2018 15:27
Note that Gagandeep is a got.lambder.
Pierre Krafft
Dec 07 2018 16:12
@Jell does this gist capture the same spirit? 36b72158c58c92b89ca2cfe05a6f8f99
Not working code but you get the idea
Jean-Louis Giordano
Dec 07 2018 16:52
f : (5 = 3 + 2, 1 + 0 = 1)
f = (Refl, Refl)
Is working code and a lost smarter than my example :p what you wrote is actually a proof, so much stronger than a unit test. My implementation was literally "if this value is False, crash compilation" for a bunch of Booleans :p
I also just remembered a good reason to not do compile-time unit tests in Idris: evaluation is really slow without type erasure
Pierre Krafft
Dec 07 2018 17:06
I really love the world of Agda and Idris 😀
Having types and values mixed makes for a completely new way of thinking about your programs
Very very fun experience