Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

crufter.com

Post reply on HN
Print view View original

91–100 of 101 posts

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

#91

Post by pathsjs »

lomnakkus wrote: post #90
pathsjs wrote: post #89

Earlier quoted context omitted.

I will try to be more clear. Say the size is actually unknown until runtime, for instance a vector is read from a file. You cannot apply directly any of the size-aware functions, because it will not typecheck. I only see two avenues: Either you assert statically that the vector has some concrete size, in which case the size is known statically and the code generation will work as well; Or you use some other size-unaw…

> I will try to be more clear. Say the size is actually unknown until runtime, for instance a vector is read from a file. You cannot apply directly any of the size-aware functions, because it will not typecheck. Yes, you can in fact do that! Let's assume you're building the list you're reading from a file as if it were a linked list. That's the point of dependent types -- the types can (and often do) depend on run-ti…

Ok, I see how it can work. Thank you very much for your explanation!

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

#92

Post by codygman »

enraged_camel wrote: post #46
skosch wrote: post #37

Earlier quoted context omitted.

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 d…

I'm more of a "learn by building things" type of learner. What kinds of things can I build with Haskell? For example, I got into Ruby via Rails, because Rails lets you quickly prototype simple web apps. So I could go from "I wish I had an app that does X" to actually building it, deploying it and sharing it with others. What would a similar "learning flow" look like in Haskell? (doesn't have to be web-based) Put anot…

This is a good tutorial for web development with Yesod:

https://pbrisbin.com/posts/developing_web_applications_with_...

You might want to try using stack instead of cabal though to ensure you avoid any dependency issues. I think cabal will work fine these days, but I have been using stack/stackage for some time so can't guarantee it.

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

#93

Post by serverholic »

solomatov wrote: post #31
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.

You can choose how rigorous you want your proof to be.

I'd highly recommend reading Chapter 1, Section 1.3 from Type-Driven Development. The first chapter is free.

https://www.manning.com/books/type-driven-development-with-i...

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

#94

Post by dllthomas »

muhuk wrote: post #86

But does it allow specifying vectors that has no less than three and no more than seven items? Or vectors with even number of items? More importantly can we possibly implement church numerals in Haskell? /rhetorical

"But does it allow specifying vectors that has no less than three and no more than seven items? Or vectors with even number of items?"

Yes.

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

#95

Post by kazinator »

a3n wrote: post #27
kazinator wrote: post #16

Earlier quoted context omitted.

> There's nothing about braces that ensures visual cues to nested code. A machine can look at the braces and re-indent the code, so that you don't have to look at the braces. All while you rest assured that the meaning didn't change: I just popped it into Vim, selected all and hit =: int func() { while dosomething() { dosomething() dosomething() doanotherthing() } dosomething() } Some semicolons are expected so thing…

The braces didn't do anything for a human until indentations were added, whether by human or machine. If you lifted those braces out, you'd still know that the intent was (although in C it would be wrong :) The only thing I miss about braces is being able to jump to the end of a block easily. In python and similar that's a bit harder to do with an editor.

> If you lifted those braces out, you'd still know that the intent was

That's also true if the intent is ambiguous (the braces say one thing and the indentation something else).

Hey, remove the braces and the intent is clear now!

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

#96

Post by kazinator »

a3n wrote: post #27
kazinator wrote: post #16

Earlier quoted context omitted.

> There's nothing about braces that ensures visual cues to nested code. A machine can look at the braces and re-indent the code, so that you don't have to look at the braces. All while you rest assured that the meaning didn't change: I just popped it into Vim, selected all and hit =: int func() { while dosomething() { dosomething() dosomething() doanotherthing() } dosomething() } Some semicolons are expected so thing…

The braces didn't do anything for a human until indentations were added, whether by human or machine. If you lifted those braces out, you'd still know that the intent was (although in C it would be wrong :) The only thing I miss about braces is being able to jump to the end of a block easily. In python and similar that's a bit harder to do with an editor.

The language being discussed has parentheses and brackets:

    Vect n a -> Vect m a -> Vect (n + m) a
What's that around n + m, and how eager are you to replace that with multi-line indentation?

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

#97

Post by kmicklas »

kazagistar wrote: post #58
dllthomas wrote: post #53

Earlier quoted context omitted.

Almost arbitrarily - they must be computable... ;)

From what I know, Idris does not have this constraint: you are free to introduce nontermination wherever.

You're correct that Idris doesn't force termination. That doesn't let you compute non-computable functions though (e.g. the busy beaver function).

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

#98

Post by lomnakkus »

pathsjs wrote: post #91
lomnakkus wrote: post #90

Earlier quoted context omitted.

> I will try to be more clear. Say the size is actually unknown until runtime, for instance a vector is read from a file. You cannot apply directly any of the size-aware functions, because it will not typecheck. Yes, you can in fact do that! Let's assume you're building the list you're reading from a file as if it were a linked list. That's the point of dependent types -- the types can (and often do) depend on run-ti…

Ok, I see how it can work. Thank you very much for your explanation!

Actually, I see that I was a bit sloppy in that post wrt. the type annotations and editing, but I'm glad it helped :).

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

#99

Post by a3n »

kazinator wrote: post #96
a3n wrote: post #27

Earlier quoted context omitted.

The braces didn't do anything for a human until indentations were added, whether by human or machine. If you lifted those braces out, you'd still know that the intent was (although in C it would be wrong :) The only thing I miss about braces is being able to jump to the end of a block easily. In python and similar that's a bit harder to do with an editor.

The language being discussed has parentheses and brackets: Vect n a -> Vect m a -> Vect (n + m) a What's that around n + m, and how eager are you to replace that with multi-line indentation?

That's an expression, not a code block. I would not want to replace that with anything.

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

#100

Post by a3n »

kazinator wrote: post #95
a3n wrote: post #27

Earlier quoted context omitted.

The braces didn't do anything for a human until indentations were added, whether by human or machine. If you lifted those braces out, you'd still know that the intent was (although in C it would be wrong :) The only thing I miss about braces is being able to jump to the end of a block easily. In python and similar that's a bit harder to do with an editor.

> If you lifted those braces out, you'd still know that the intent was That's also true if the intent is ambiguous (the braces say one thing and the indentation something else). Hey, remove the braces and the intent is clear now!

Yes there are advantages to braced blocks. I sometimes miss them, but mostly not.
Post reply on HN