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

71–80 of 101 posts

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

#71

Post by a3n »

pdkl95 wrote: post #42
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 braces didn't do anything for a human until indentations were added Having explicit delimiters (I don't care if it's {}, begin...end, or whatever) provide several benefits that I have often used. 1. (by far the most important) They trivialize the recovery of indentation that has been trashed by a bad/misconfigured/unfamiliar editor or coworker who inserted "\t" characters into the file. Just run indent-region o…

I do like rainbow delimiters. Parens and others show up nicely.

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

#72

Post by a3n »

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.

> although in C it would be wrong

Meaning that without the braces the code itself would be wrong, in C. Not that C itself is wrong.

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

#73

Post by Ixiaus »

cheepin wrote: post #64
Ixiaus wrote: post #50

Earlier quoted context omitted.

Warning: highly biased opinion incoming. I came from Python to Erlang / Scheme / Haskell and at this point I would answer your question, > What kind of things can I build with Haskell? With: Everything. We use Haskell in production at Plum for our REST APIs, job schedulers, web applications, AWS service interfaces, a static site compiler, DB modeling, command line utilities, etc... We also use it for two CLI utilitie…

> With: Everything. This may be nitpicking but certain classes of programs cannot be realistically built with Haskell. Anytime you need to tightly control latency (soft realtime) won't really work since you have both a garbage collector and lazy evaluation. Memory constrained systems are pretty tough as well since you don't really get insight into allocation/deallocation, which also makes structuring your data into a…

Yes, that's a good point of clarification, one that the Ivory or Atom DSL is trying to tackle though.

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

#74

Post by rfw »

dllthomas wrote: post #49
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.

Per my understanding, what's so exciting about this is precisely that you're wrong - it does not need to be known at compile time, but can prove symbolically that the resulting length will be X + Y. And of course, given that, it's not statically creating a distinct instantiation of the Vect type for every N at compile time!

Really? Color me corrected, then :) Does the compiler need a SAT solver then to make sure all the constraints hold?

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

#75

Post by Ixiaus »

dllthomas wrote: post #69
cheepin wrote: post #64

Earlier quoted context omitted.

> With: Everything. This may be nitpicking but certain classes of programs cannot be realistically built with Haskell. Anytime you need to tightly control latency (soft realtime) won't really work since you have both a garbage collector and lazy evaluation. Memory constrained systems are pretty tough as well since you don't really get insight into allocation/deallocation, which also makes structuring your data into a…

This depends on what you mean by "with". As you say, you can't sit down, bang out some ordinary Haskell code, and expect GHC to give you an executable that will do real-time as well as you can in C. That said, it's perfectly possible to write a DSL that handles scheduling, uses GHC's type machinery to track memory use and execution time, and have GHC generate a program that will generate C code that meets hard real-t…

This as well: http://ivorylang.org/ivory-introduction.html

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

#76

Post by andreaferretti »

pcwalton wrote: post #65
tines wrote: post #45

Earlier quoted context omitted.

As a C++ programmer, I'd like to ask how is this different in effect from template std::array app(std::array , std::array );

Because with dependent typing, the length can be specified at runtime and you still get static checking. There's also a huge difference between untyped templates and strongly typed generics, but in this particular case the difference is somewhat subtle.

How does it work exactly? Both languages check things at compile time, but of course in c++ the length has to be known statically. Does idris generate code at runtime for the right size?

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

#77

Post by pzone »

rfw wrote: post #74
dllthomas wrote: post #49

Earlier quoted context omitted.

Per my understanding, what's so exciting about this is precisely that you're wrong - it does not need to be known at compile time, but can prove symbolically that the resulting length will be X + Y. And of course, given that, it's not statically creating a distinct instantiation of the Vect type for every N at compile time!

Really? Color me corrected, then :) Does the compiler need a SAT solver then to make sure all the constraints hold?

It should be able to use a Hindley-Milner algorithm.

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

#78

Post by dllthomas »

rfw wrote: post #74
dllthomas wrote: post #49

Earlier quoted context omitted.

Per my understanding, what's so exciting about this is precisely that you're wrong - it does not need to be known at compile time, but can prove symbolically that the resulting length will be X + Y. And of course, given that, it's not statically creating a distinct instantiation of the Vect type for every N at compile time!

Really? Color me corrected, then :) Does the compiler need a SAT solver then to make sure all the constraints hold?

I'm not sure the exact approach, but there's definitely some heavy lifting. My understanding is that most (all?) dependently typed languages are essentially theorem provers at heart.

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

#79

Post by dllthomas »

pzone wrote: post #77
rfw wrote: post #74

Earlier quoted context omitted.

Really? Color me corrected, then :) Does the compiler need a SAT solver then to make sure all the constraints hold?

It should be able to use a Hindley-Milner algorithm.

As I understand it, type inference breaks down on dependent types.

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

#80

Post by chenglou »

andreaferretti wrote: post #76
pcwalton wrote: post #65

Earlier quoted context omitted.

Because with dependent typing, the length can be specified at runtime and you still get static checking. There's also a huge difference between untyped templates and strongly typed generics, but in this particular case the difference is somewhat subtle.

How does it work exactly? Both languages check things at compile time, but of course in c++ the length has to be known statically. Does idris generate code at runtime for the right size?

Think about generics in any language, say Java Stack. The type Stack is parametrized by the type String. What would you do in a language without generic types? To achieve the same effect, you'd need to create a custom StackString type, which itself is trivial. But then, you'd need StackInteger, StackBoolean, StackSomeoneElsesCustomType, etc.

Language with a type system but without generics have this above downside. Usually you'd just give up making a type for each of these, and simply use the Stack type.

Language without Idris-like dependent types suffer the same downside: instead of creating Stack, you're forced to create Stack, Stack, Stack, where One/Two/Three are unique types you created to conceptually represent a number. If you don't even have generics, you'd need to create StackStringOne, StackStringTwo, ...

Dependently typed languages encode numbers (among others) as unique types, to simplify. Imagine this:

  put: Stack -> String -> Stack
This isn't too hard to imagine is it? No runtime checks needed. Once you get the output you can carry it around, along with its type, to places that accept Stack.

So, asking "how come you don't have to generate these checks at runtime?" is similar to a programmer who's never seen generics asking "how come you can parametrize? Don't you have to generate all the StackString and StackInteger, etc.". It just works. Hope that analogy was clear =).

Dependent types in general blur the line between values and types, as you've seen above. Think of the usual values you use, and imagine having a new type to represent each one. Dependent types let you do this in a sane and logical way.

Post reply on HN