The idea and approach is brilliant. I hope it's the next big thing in programming.
I'm quite sure Haskell didn't get mainstream because of it's non-strict evaluation. It's just too alien. Everything else: syntax, types, FP, typeclasses, monads... are EASY in comparison. Haskell heritage is useful as people can copy-paste a big set of tested solutions to their Lazy libraries. But for me it's "Opt-in laziness > Opt-out laziness" from now on.
Swap between : and :: suits well for Idris.
List String instead of [String] (PureScript did that too!).
This is insanely good.
Idris> the (List _) ["Hello", "There"]
["Hello", "There"] : List String
Idris> the (Vect _ _) ["Hello", "There"]
["Hello", "There"] : Vect 2 String
Haskell-like abomination:
import SomeModule -- @_@
I caught myself to find (real) Haskell code plainly undreadable way too often. I just couldn't trace functions to their host packages. So basic and so annoying.
Idris> :doc List
...
(::) : (x : elem) -> (xs : List elem) -> List elem
-- instead of a MORE readable
(::) : a -> List a -> List a
I believe that x and xs add nothing to the picture except a visual noise. I hate TypeScript for it's Java-like type syntax
with ugly and unclear type signatures which you need to decipher every time you see them. I'm afraid Idris is leaning to the same direction.
It's still (String, Bool) instead of Tuple String Bool. Seems not consistent. PureScript did that better I guess.
Almost all of them are not helpful. It's like Haskell telling you to enable some magical extension when you just miss a comma...
Something about List (singular) vs Strings (plural) bugs me, and you see those two together a lot.
TDD with Idris – awesome book. More readable than all Haskell books I tried(!)
Used Atom. Relied only on syntax highlighting. Nothing to say for now.
Community is super small. Don't expect to find help as IRC is empty and mailing list is silent so to say.
Idris> :let square : Double -> Double
Idris> :let square x = x * x
When checking an application of function Prelude.Interfaces.*:
No such variable x ??? @_@
Idris> :let square : Double -> Double ; square x = x * x
(input):1:13:square already defined ??? @_@
(input):1:13:square is already defined ??? @_@
Idris> square 2
square 2.0 : Double ??? @_@
So how to declare multi-line function in REPL? I've found no such examples at docs or GitHub :(
Idris> :t \x => x + x
\x => x + x : Integer -> Integer ??? @_@ why not Num a => a -> a
Idris> (\x => x + x) 2.0
4.0 : Double ??? @_@ so Integer or Double
Works:
wordCount : String -> Nat
wordCount str = length (words str)
average : (str : String) -> Double
average str = let numWords = wordCount str
totalLength = sum (allLengths (words str)) in
cast totalLength / cast numWords
where
allLengths : List String -> List Nat
allLengths strs = map length strs
Fails at #1:
wordCount : String -> Nat
wordCount str = length (words str)
average : (str : String) -> Double
average str = let numWords = wordCount str
totalLength = sum (map length (words str)) in -- #1
cast totalLength / cast numWords
with the message
When checking right hand side of average with expected type
Double
Can't disambiguate since no name has a suitable type:
Prelude.List.length, Prelude.Strings.length
the solution is to add namespace Strings.length to the map length call.
Another example of the same(?) name disambiguation weirdness:
Works:
topTen : Ord a => List a -> List a
topTen xs = take 10 $ reverse $ sort xs
Fails:
topTen : Ord a => List a -> List a
topTen xs = (take 10 . reverse . sort) xs
with the message: Can't disambiguate name: Prelude.List.take, Prelude.Stream.take
Works again:
topTen : Ord a => List a -> List a
topTen xs = (List.take 10 . reverse . sort) xs
I hit several of those in total. So I wonder:
- Should I just always use namespaces to avoid such traps?
- Why support function overload at all. It just fails too often imo...
Works:
module Main
palindrome : String -> Bool
palindrome s = s1 == reverse (toLower s)
where s1 = toLower s
Fails at #1:
module Main
palindrome : String -> Bool
palindrome s = s1 == s2 -- #1
where s1 = toLower s
s2 = reverse (toLower s)
with the message Can't find implementation for Eq ty. From the docs I understood that where is for functions and let is for variables (not sure a requirement or a convention) but why one variable works and two – don't?! @_@