Idris, a language that will change the way you think about programming (2015) • Hacker News Board

Re: Idris, a language that will change the way you think about programming (2015)

#31

Post by solomatov » Thu, Jan 07, 2016, 4:26 AM UTC

bojo wrote: post #17

app : Vect n a -> Vect m a -> Vect (n + m) a That is pretty amazing if you ask me. I look forward to the day when we all use languages which save programmers from themselves.

Actually it's not that easy. Everywhere you have a type you need to proof that the expression really has the right type, and it's not just type annotation, it's a real mathematical proof.

To understand the complexity of the task, try proving that insertion sort is really a sort algorithm. You write more code, and writing it will take more time than you would do in a 'normal' typed language.

Re: Idris, a language that will change the way you think about programming (2015)

#32

Post by pekk » Thu, Jan 07, 2016, 4:28 AM UTC

spo81rty wrote: post #30

a3n wrote: post #15

Earlier quoted context omitted.

There's nothing about braces that ensures visual cues to nested code. Significant whitespace does precisely that. And eliminates brace placement arguments. int func() { while dosomething() { dosomething() dosomething() doanotherthing() } dosomething() } def func(): while dosomething(): dosomething() dosomething() doanotherthing() dosomething()

I've never used a language where space indentation was used over curly brackets. So question for those who have... When doing so, wouldn't copying and pasting code around potentially cause a lot of accidental issues? Are there some negatives and side effects of the indentation style? Just curious.

If you copy and paste code irrespective of bracket position, you will have the same problems. It turns out not to be an issue.

A big positive of using indentation is that it enforces a visual indication of scope vs. languages where culturally it is normal to find code with lots of giant one-liners and braces on one line.

But overall, you just get used to it and don't notice it. Everyone who yells about languages that use indentation is bikeshedding in the worst way.

Re: Idris, a language that will change the way you think about programming (2015)

#33

Post by solomatov » Thu, Jan 07, 2016, 4:28 AM UTC

If you are interested in Idris, you might also be interested in agda, which is another dependently typed programming language: https://en.wikipedia.org/wiki/Agda_(programming_language)

Re: Idris, a language that will change the way you think about programming (2015)

#34

Post by farhanhubble » Thu, Jan 07, 2016, 4:32 AM UTC

Thanks for the link. I was looking into liquid Haskell and refinement types and thought that it's a great idea but rued the fact that it wasn't built into the language. I am definitely going to try Idris for one of my projects.

Re: Idris, a language that will change the way you think about programming (2015)

#35

Post by rfw » Thu, Jan 07, 2016, 5:09 AM UTC

bojo wrote: post #17

app : Vect n a -> Vect m a -> Vect (n + m) a That is pretty amazing if you ask me. I look forward to the day when we all use languages which save programmers from themselves.

Unfortunately, the usefulness is limited – the size of all Vects must be known at compile time. While this does prevent a large class of bugs that arise from incorrect compile-time knowledge, the size of the class of runtime bugs affected by this is a lot smaller, as for each differently-lengthed Vect, a distinct instantiation of the Vect type needs to exist at compile-time.

Re: Idris, a language that will change the way you think about programming (2015)

#36

Post by andolanra » Thu, Jan 07, 2016, 5:18 AM UTC

ophelia wrote: post #3

Is Idris related to Idris Elba, the British actor, by any chance?

The story, if I recall correctly, is that the programmer Edwin Brady had a previous project that was a proof engine, and lacking a suitable name for it, named after an older British children's cartoon called Ivor the Engine.[^1] When it came time to name a newer project, he decided to name it after another character from the same show: Idris, the little red Welsh dragon. This, incidentally, is why the Idris language's logo is a stylized red wing.

[^1]: Ivor the Proof Engine is here, although apparently not actively updated any more: https://github.com/edwinb/Ivor

Re: Idris, a language that will change the way you think about programming (2015)

#37

Post by skosch » Thu, Jan 07, 2016, 5:18 AM UTC

athesyn wrote: post #18

Bit disappointed it makes the assumption the reader knows Haskell, that lost me immediately.

You know what, I've found it immensely valuable to get acquainted with Haskell, even though I've never used it (and likely never will). The concepts are timelessly beautiful, simple to understand, and can feel enlightening to run-of-the-mill imperative/OOP programmers.

What's more, it seems to me that Haskell syntax is the lingua franca when discussing anything related to data types and functional programming these days. Those ->'s are everywhere, it's useful to know what they stand for.

Just skim a few chapters of learnyouahaskell.com; you won't regret it.

Re: Idris, a language that will change the way you think about programming (2015)

#38

Post by kmicklas » Thu, Jan 07, 2016, 5:23 AM UTC

rfw wrote: post #35

bojo wrote: post #17

app : Vect n a -> Vect m a -> Vect (n + m) a That is pretty amazing if you ask me. I look forward to the day when we all use languages which save programmers from themselves.

Unfortunately, the usefulness is limited – the size of all Vects must be known at compile time. While this does prevent a large class of bugs that arise from incorrect compile-time knowledge, the size of the class of runtime bugs affected by this is a lot smaller, as for each differently-lengthed Vect, a distinct instantiation of the Vect type needs to exist at compile-time.

Not quite. Types can depend on runtime values. This can in effect _force_ the programmer to perform the required validation when accepting foreign data.

Re: Idris, a language that will change the way you think about programming (2015)

#39

Post by nihils » Thu, Jan 07, 2016, 5:24 AM UTC

This is actually perfect for a library on algebraic structures I've been trying to make in Haskell. For example, how does one distinguish between elements in the Dihedral group of order 10 vs. Dihedral group on order 16 when obstensibly, they have the same representation. For now, I think Haskell programmers use type-level arithmetic libraries, but this is a much better solution.

Re: Idris, a language that will change the way you think about programming (2015)

#40

Post by lambdasquirrel » Thu, Jan 07, 2016, 5:27 AM UTC

kmicklas wrote: post #38

rfw wrote: post #35

Earlier quoted context omitted.

Unfortunately, the usefulness is limited – the size of all Vects must be known at compile time. While this does prevent a large class of bugs that arise from incorrect compile-time knowledge, the size of the class of runtime bugs affected by this is a lot smaller, as for each differently-lengthed Vect, a distinct instantiation of the Vect type needs to exist at compile-time.

Not quite. Types can depend on runtime values. This can in effect _force_ the programmer to perform the required validation when accepting foreign data.

Not only that but you can arbitrarily encode constraints. Want to check something silly like whether there's an even number of elements in a list? Yea you can do that, and pass it along. I can do stuff like, okay, I know the max size of the files we're going to accept is 1mb.