exercism / idris

Exercism exercises in Idris.
https://exercism.org/tracks/idris
MIT License
32 stars 18 forks source link

Add default introductory code example #32

Closed kytrinyx closed 7 years ago

kytrinyx commented 7 years ago

Instead of having logic for a fallback in the backend, we're choosing a default for the snippet file.

For tracks that have core exercises, we pick the first core exercise. For tracks without these, we pick the first exercise listed in the config.

Note that we're aiming for 10 lines and a max-width of 40 columns. This solution has a max-width of 61, so we may want to adjust it.

See https://github.com/exercism/meta/issues/89

kytrinyx commented 7 years ago

I think we should just remove the conditional. I don't actually know Idris so I hesitate to mess with this (I know I can figure it out, but I'd totally rather accept someone else's PR and close this one). If you do submit something, would you mind @mentioning me or dropping a line in here so I get the notification?

yurrriq commented 7 years ago

How do you mean, conditional? IIUC we could do something like one of the following:

kytrinyx commented 7 years ago

How do you mean, conditional

Sorry, I mean the bit where it's either "world" or the name that gets passed in:

greet subject = "Hello, " ++ fromMaybe "World" subject ++ "!"

Do you have a preference? I'm leaning towards the 37x6 wide one, since it fits, but if you think it doesn't do a good job showing off the language, the Leap one would also be great.

yurrriq commented 7 years ago

I'm cool with whatever, but none of these examples really show off the language. I'm thinking an isEven along the lines of this discussion could be good. I'll write something up later or tomorrow.

kytrinyx commented 7 years ago

none of these examples really show off the language.

Yeah, that's what I was worried about.

I'll write something up later or tomorrow.

Sweet, thanks!

yurrriq commented 7 years ago

After golfing for a while, I've decide to borrow (and slightly modify) the following from @puffnfresh's blog for a nice, 37x10 example that gives a taste of the powerful type system:

module EvenOdd

data Even : Nat -> Type where
  EZ : Even Z
  ES : Even n -> Even (S (S n))

total
ee : Even n -> Even m -> Even (n + m)
ee EZ m     = m
ee (ES n) m = ES (ee n m)

If at all possible, we should link the blog (assuming that's cool), since this probably doesn't mean much on its own to newcomers..

kytrinyx commented 7 years ago

Could we have a shortened URL as a comment in the code example?

kytrinyx commented 7 years ago

(Also: this is a great code example!)

puffnfresh commented 7 years ago

I don't need attribution, just ship it :heart: :ship:

kytrinyx commented 7 years ago

@puffnfresh that's awesome thank you. 🚢 'd it!

yurrriq commented 7 years ago

My PR was for this branch, so I'm not sure it got merged..

kytrinyx commented 7 years ago

D'oh. That's what I get for being too quick.

kytrinyx commented 7 years ago

Let's try this again.

yurrriq commented 7 years ago

LGTM