11 ms·

Idris: A language for type-driven development

peter_d_sherman 4y ago
>"In Idris, types are first-class constructs in the langauge. This means types can be passed as arguments to functions, and returned from functions just like any other value, such as numbers, strings, or lists. This is a small but powerful idea, enabling: o Relationships to be expressed between values; for example, that two lists have the same length. o Assumptions to be made explicit and checked by the compiler. For example, if you assume that a list is non-empty, Idris can ensure this assumption always holds before the program is run. o If desired, properties of program behaviour to be formally stated and proven." PDS: I'd be curious to know about any/all languages where types can be passed to functions, returned from functions -- and even generated at runtime by functions... that is, where the language regards types as first-class constructs...
- kitd 4y ago
  This is presumably not what you're thinking of but ofc Javascript uses objects as prototype "types". As is, they wont provide what you want, but if there was some kind of "compile-time" processing of prototypes such that types assemblies, dependencies, constraints and other relationships could be manipulated or asserted before they were applied in runtime code, that may provide some of the "first-class type" functionality mentioned. Ed: actually, Typescript might be a better host for this.
  - eckza 4y ago
    FP Or Die Gang is downvoting you, but this is actually correct. No referential transparency (among other things, no doubt) makes this a harder problem to solve than just using a language that supports it. $0.02
    - still_grokking 4y ago
      If you don't have referential transparency mathematical equations don't hold. You can't be sure that `a = b` stays true if deducted once. So "the problem" doesn't get only harder, it becomes impossible to solve in a formal way.
      - eckza 4y ago
        Thank you for this. That's exactly what I was getting at; you illustrated it far better.
  - still_grokking 4y ago
    The down-votes are likely because the example isn't anyhow good. But the idea to have static prototype types is imho quite interesting on its own. I was thinking a lot about that in the past. I would love to have JS like objects—but in a static context. Row polymorphism and extensible records are close but still not there actually.
- teddyh 4y ago
  > PDS: I'd be curious to know about any/all languages where types can be passed to functions, returned from functions -- and even generated at runtime by functions... that is, where the language regards types as first-class constructs... Python does this.
  - ihm 4y ago
    These types are statically checked (i.e., can be checked before runtime).
    - teddyh 4y ago
      I was not replying to the article, I was replying to the question from “peter_d_sherman” asking if any other programming language has types as first-class constructs. And Python does that.
      - peter_d_sherman 4y ago
        Sure! I'll accept Python into the list of languages that have types as first-class constructs! And thanks, the suggestion is much appreciated!
      - typedfalse 4y ago
        Eh, in this context those aren't types; instead Python is unityped. Agreed they are still fun though.
        xigoi 4y ago
        Python is dynamically typed, but definitely not untyped.
        wk_end 4y ago
        typedfalse wrote "unityped", not "untyped" (note the "i"). When type system people talk about types they're implicitly talking about static types, rather than what Python might call a type. Robert Harper lays out the argument [0] that Python is basically a statically typed language with many "classes" but a single type - that's where I was first exposed to this idea. > The characteristics of a dynamic language are [that] values are classified [...] into a variety of forms that can be distinguished at run-time. A collection of values can be of a variety of classes, and we can sort out at run-time which is which and how to handle each form of value. Since every value in a dynamic language is classified in this manner, what we are doing is agglomerating all of the values of the language into a single, gigantic (perhaps even extensible) type. To borrow an apt description from Dana Scott, the so-called untyped (that is “dynamically typed”) languages are, in fact, unityped. Rather than have a variety of types from which to choose, there is but one! > And this is precisely what is wrong with dynamically typed languages: rather than affording the freedom to ignore types, they instead impose the bondage of restricting attention to a single type! Every single value has to be a value of that type, you have no choice! Even if in a particular situation we are absolutely certain that a particular value is, say, an integer, we have no choice but to regard it as a value of the “one true type” that is classified, not typed, as an integer. Conceptually, this is just rubbish, but it has serious, tangible penalties. For one, you are depriving yourself of the ability to state and enforce the invariant that the value at a particular program point must be an integer. For another, you are imposing a serious bit of run-time overhead to represent the class itself (a tag of some sort) and to check and remove and apply the class tag on the value each time it is used. [0] https://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-languages/ https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...
- ihm 4y ago
  The most famous ones off the top of my head: Coq, Agda, Lean, Idris, ATS. Here's a list: https://en.wikipedia.org/wiki/Category:Dependently_typed_languages https://en.wikipedia.org/wiki/Category:Dependently_typed_lan...
  - peter_d_sherman 4y ago
    That (and pages like that) are what I was looking for! Thanks, much appreciated!
    - still_grokking 4y ago
      Scala is missing on that list (even it doesn't have "full dependent types" Match-Types are quite close).
  - eggy 4y ago
    I tried ATS after finding Rust difficult. Zig is becoming my C replacement, and ATS is like a C++ replacement, although, I am using SPARK2014 now, but I am looking into ATS' contracts. There is no lack of PLs as a tool for whatever you may need to do nowadays. It's refreshing compared to 1970s to 1980s for me.
- deleted 4y ago
  [deleted]
- csande17 4y ago
  Zig is probably the closest you'll get to this in an imperative language. You can write functions that take types as arguments and return types, and that's how e.g. generic data structures are implemented.
  - astrange 4y ago
    You can do that in Smalltalk descendants, if by types you mean metaclasses.
    - still_grokking 4y ago
      No, types are not runtime values! That's the whole point. That's why dependent types are so special (and complicated): You can use them as first class constructs without them being runtime values ever. Everything happens in the type checker. At runtime there are no types in proper static languages; things like Java / C# are actually quite dynamic in contrast; the dynamic nature was even part of the marketing of those languages back than. (Runtime) reflection is just dynamic typing…
      - astrange 4y ago
        "Runtime value" is an implementation detail. You could write an Idris interpreter. It'd be useful too. Why should your whole project fail to run just because one file that's not going to get used has a type error?
        still_grokking 4y ago
        > "Runtime value" is an implementation detail. You could write an Idris interpreter. Sure. And such an interpreter would still not interpret types at runtime, as types are not (runtime) values. Only at type-checking time (which is of course a phase before the program actually runs / gets interpreted) you would do anything with the types. > It'd be useful too. Why should your whole project fail to run just because one file that's not going to get used has a type error? Whether that would be anyhow "useful" depends on the definition of "file usage". If there's any reference form the "used" parts of the program to the "unused file" you have a problem: A type error (in a language where "programs as proves" is a thing) means that you "proved" false. But form a "prove" of false you can "prove" anything! So you actually lost all proving power. Your program may now explode at runtime with arbitrary type errors anywhere. At that point your "static type system" becomes completely useless. (Of course, if nothing in your "unused file" is referenced anywhere in the "used" files, noting happens. But in this case that "unused file" isn't part of your program, so it's completely irrelevant what's inside anyway.)
- skybrian 4y ago
  Zig does some of this. Functions can be written that can be called at compile time or runtime, depending on which language features they use. Types can be computed and returned by functions in compile-time expressions. I don't know how expressive the types can get, though?
  - Avshalom 4y ago
    I'm going to guess not very expressive. Zig refuses to have operator overloading because it might be used to call a function that's more expensive than you'd guess so the idea that they'd let types enforce all that much seems unlikely.
  - still_grokking 4y ago
    You can pass "types" also around in C#… But in both cases that aren't types in the sens of type theory. In both cases those are just regular values (of type "Type"). In both cases you will be able to find those values with the help of a debugger. (The difference between Zig and C# being that in Zig those values are constructed during compilation and than mostly thrown away again whereas the "type" values are just regular runtime data on the CLR).
    - skybrian 4y ago
      The types created in compile-time code are just as "real" as the types you declare in source code. All types become values at compile time. When you write a compiler, the parser creates ordinary values, perhaps instances of a Type type. The type-checking code operates on these values to find errors according to the rules of type theory. Compile-time functions are a way of calling user-defined code in the compiler, much like a macro but saner, and they can create types that can be used in declarations, verified by the type checker, and used as input to the code generator. (Reflective use of runtime types in languages like C#, Java, or Go is different.)
      - still_grokking 4y ago
        Even you almost didn't say anything wrong here there is a key misunderstanding: The term "type theory", which I've used and to which I referred (and which you've picked up), is a technical term form math. Languages like C# or Zig are not based on type theory. What is called "types" in those languages has (mostly) no relation to type theory. Those "types" are (mostly) regular values when looked at them through the type theory lens.
- cpurdy 4y ago
  >I'd be curious to know about any/all languages where types can be passed to functions, returned from functions -- and even generated at runtime by functions... that is, where the language regards types as first-class constructs... Ecstasy (xtclang).
- still_grokking 4y ago
  The examples are completely out of context. > Relationships to be expressed between values; for example, that two lists have the same length. This can be also expressed in any language, even in unityped (a.k.a. "dynamic") ones. You don't need types for that at all… > Assumptions to be made explicit and checked by the compiler. This can be also expressed in any language, even in unityped (a.k.a. "dynamic") ones. In theory you don't need types for that at all. (Even types would be the current std. method to achieve that). > For example, if you assume that a list is non-empty, Idris can ensure this assumption always holds before the program is run. You can construct a NEL (NonEmptyList) in any language. That's trivial. You just need to enforce the usage of the right factory method for your list. > If desired, properties of program behaviour to be formally stated and proven. This has nothing to do with dependent types (directly). A language based on simply typed lambda calculus is "enough" to arrive at this property.
  - dmytrish 4y ago
    Exactly, you can ship software in unityped languages. Still, how do you express even such a simple thing as a generic list type in simply typed lambda calculus? It's just that dependent types enable you to express any invariants statically, without actually running the code. > You can construct a NEL (NonEmptyList) in any language. That's trivial. That's true, with the caveat of: this invariant only exists in your head and hopefully docs. When it's encoded in a type, your compiler gets awareness of this invariant as well. Then it's able to do things that were impossible before, it can catch bugs that you would not (e.g. due the sheer amount of source code). Even though there are other approaches to software verification, types are the only one that got mainstream adoption so far.
    - still_grokking 4y ago
      Of course. But the examples given missed the point imho. All of the stated things don't need any type level machinery. You can just test things at runtime and be good. If you want to prove things at compile time that's a very different story. But than this needs to be explicitly stated in the examples.
jshaqaw 4y ago
I'm a big fan of this book for anyone interested in the topic: https://www.amazon.com/Gentle-Introduction-Dependent-Types-Idris/dp/1723139416/ref=sr_1_2?crid=1TAWAM306Z0NE&keywords=idris+book+types&qid=1674232196&sprefix=idris+book+types%2Caps%2C82&sr=8-2 https://www.amazon.com/Gentle-Introduction-Dependent-Types-I...
- peter_d_sherman 4y ago
  Looks highly interesting... Thanks for the suggestion!
- gre 4y ago
  Better link... https://leanpub.com/gidti https://leanpub.com/gidti
  - CoastalCoder 4y ago
    Anyone know if there's a decent way to get a printed copy? Or barring that, can anyone suggest a good device on which to read it and jot notes, for someone who normally prefers printed books?
    - nerdponx 4y ago
      I bought a basic b&w two-sided laser printer in 2011 for this purpose, and it's served me extremely well over the years. You can then take the stack of pages to a store like Staples and they will bind it for you for a few dollars. I got the Brother HL-2270DW and I think they still make it. They even publish official Linux drivers for CUPS! Just make sure to get the extended toner cartridges (TN450), the regular ones are a ripoff.
      - Jtsummers 4y ago
        Staples and others will also print and bind PDFs you bring in. I've done this with purchased books, sometimes they get a bit picky but usually they'll just do it.
    - deleted 4y ago
ykonstant 4y ago
I am dabbling in the cousin language Lean right now, and it is very fun to use!
- peter_d_sherman 4y ago
  Some quick info for Lean: Homepage: https://leanprover.github.io/ https://leanprover.github.io/ Source: https://github.com/leanprover/lean4 https://github.com/leanprover/lean4 Wikipedia: https://en.wikipedia.org/wiki/Lean_(proof_assistant) https://en.wikipedia.org/wiki/Lean_(proof_assistant)
  - agentultra 4y ago
    I also wrote a guide: https://agentultra.github.io/lean-4-hackers/ https://agentultra.github.io/lean-4-hackers/
    - still_grokking 4y ago
      LEAN's syntax looks really great. I wish Scala could take some inspiration. Scala's syntax is anyway quite similar already, but would need proper Unicode support and some other "tuning" like the `:=` and the `let monadic ← effect` syntax, imho.
- daxfohl 4y ago
  One difference I see is Lean uses type classes while Idris uses implicits. Can anyone comment on the pros and cons of that decision? (Or pros and cons between the two languages in general?) It also seems that Idris was created as a general-purpose language first, whereas Lean started as a proof assistant and only recently added general-purpose language. Is that evident when using the languages? A quick look at Lean's general-purpose language seems reasonably similar to the Indris experience AFAICT.
  - ImprobableTruth 4y ago
    Imo the biggest difference is the "heritage", Lean is Coq inspired, Idris Agda inspired. This manifests in how people prove things. Idris has dependent pattern matching, so proofs are written as normal terms. Lean has tactics and proofs are small tactics scripts (which then generate the proof term behind the scene). Other than that, the difference is mainly in infrastructure/libraries and community.
peter_d_sherman 4y ago
There also seems to be some intersection here between type-driven development and Proof Assistants: https://en.wikipedia.org/wiki/Proof_assistant https://en.wikipedia.org/wiki/Proof_assistant
- jshaqaw 4y ago
  A huge overlap. Idris is aimed at being a general purpose language with proof assistant characteristics while some of its peers are more theorem provers built with general purpose language characteristics.
- chills 4y ago
  See also: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
  - peter_d_sherman 4y ago
    Wowzer! That is quite the page... There is definitely something there! That page is decidedly worth reading and re-reading many times in the future... I think it boils down to the following: >"Curry–Howard correspondence [...] is the direct relationship between computer programs and mathematical proofs." And: >"If one abstracts on the peculiarities of either formalism, the following generalization arises: a proof is a program, and the formula it proves is the type for the program." In fact, I'm going to go for "full crackpot" here... If all computer programs are algorithms, and all mathematical proofs are algorithms, and all types are algorithms -- then a "grand unifying theory" between Computer Programs and Mathematics -- looks like this: It's all Algorithms. Algorithms on top of algorithms. You know, like turtles on top of turtles... This makes sense too, if we think about it... Algorithms are just series of steps, with given inputs and given outputs. That is no different than Computer Programs. And that is no different than Math... You can call this series of steps an Algorithm, you can call it a Function, you can call it y=f(x), you can call it a Type, you can call it a Computer Program, you can call it a Math Equation, you can call it a logical proposition, and you can use whatever notation and nomenclature you like -- but in the end, in the end, it all boils down to an Algorithm... A series of steps... Now, perhaps that series of steps -- uses other series of steps -- perhaps that Algorithm uses other Algorithms, perhaps that function uses other functions, perhaps that Computer Program uses other computer programs, perhaps that Math Equation uses other math equations, etc., etc. -- But in the end, in the end... It's all a series of rigorously defined steps... It's all an Algorithm... Or Algorithm consisting of other Algorithms... (recursively...) Patterns of steps -- inside of patterns of other steps (again, recursively...) Anyway, great page, definitely worth reading and re-reading!
nightowl_games 4y ago
Anyone else finding this documentation is pretty hard to navigate? Makes me think this isn't a serious language, but rather an academic toy or resume builder.
- andrewmcwatters 4y ago
  The main repository is in the top 1% of stargazed repositories on GitHub, and the project has a mailing list, Discord server, IRC, AND Slack. It has been forked over 300 times, and has over 100 contributors. What in the world counts as "serious" to some of you people? Sometimes I read HN and ask myself if people here know at all how hard it is make something people want, and how many people know what the real-world thresholds are for understanding when you have made something that people want. I guess if everyone hasn't heard of it, people here don't think it's serious.
  - bobleeswagger 4y ago
    [flagged]
    - andrewmcwatters 4y ago
      I mean you tell me, which would be bullying to you? You work for years on something and someone tells you it's not "serious" because they haven't learned to browse a source tree, or the guy telling him to read a little more? Either way, I apologize for how it came off.
      - bobleeswagger 4y ago
        > someone tells you it's not "serious" because they haven't learned to browse a source tree "Fuck this stranger for not learning something I know how to do!"
  - mejutoco 4y ago
    I find Idris incredibly interesting. Specially combined with the output it can generate in other languages. The book of it is also a masterpiece, even if you never program in it. Already lots of "serious" hacked together programming languages. The only downside I see if the lack of a package manager.
satvikpendem 4y ago
The book itself Type Driven Development with Idris is great too, it is the principal way I write code these days, by writing my types upfront then filling out the logic, and in some languages, the logic itself can be produced automatically via the filling of type holes. In other words, simply based on the types you provide, the compiler can guess the implementation of the function, somewhat like Copilot but guaranteed to be correct on a type level, even if not necessarily on a business logic level. https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...
- acchow 4y ago
  I had never heard of this book before, now I definitely want to give it a try. As an aside, isn't type driven development how everyone codes naturally in statically typed languages? Whether it's Ocaml or Java, I feel like I try to get the types defined, then put on music and turn my brain off and just line the types up (much moreso in Ocaml than in Java).
  - satvikpendem 4y ago
    Indeed, and this is precisely why I hate writing in dynamically typed languages like Ruby or Python; they hinder me from thinking about the shape of the program clearly.
    - iddan 4y ago
      Well now you can write full types in both of them
      - shpongled 4y ago
        You can write them, but without most of the benefits of static types
        mejutoco 4y ago
        You can typecheck them with mypy or pyright or at runtime with typeguard. It is not ideal, but pretty good in terms of benefits.
spelunker 4y ago
Here's an intro to dependent types from David Christiansen, I think it came up during another dependent types discussion: https://youtu.be/VxINoKFm-S4 https://youtu.be/VxINoKFm-S4
theresistor 4y ago
What's the state of Idris2 at this point? I really enjoyed Type Driven Development with Idris a few years ago.
- still_grokking 4y ago
  It's the current version. https://www.idris-lang.org/idris-2-version-060-released.html https://www.idris-lang.org/idris-2-version-060-released.html Idris 1 seems obsolete since years. No news about it for a long time. https://www.idris-lang.org/category/news.html https://www.idris-lang.org/category/news.html
mcdonje 4y ago
I know I'm missing something, but this seems like the functional version of object classes. I've mostly favored procedural programming and only use objects when I have to because the abstraction can make the program harder to reason about, especially when there's a lot of inheritance. But I've heard some hype about types in Rust, and now this. The free chapter in the manning book even introduces types in terms of real world objects. So, for someone who doesn't love objects, why should I love types?
- ok_dad 4y ago
  Where objects can hide state or I/O in a program, types and functional type driven development make each function very clear as to what it has for input and outputs and part of that is not hiding state anywhere that doesn’t make sense. You might still have a global logger because that makes sense, but generally you know the things you have access to because they’re in the function signature. It can break down if you aren’t careful, and there’s some nuance where you might still store a configuration data as an object property, but it’s a clearly typed property that’s assigned at initialization rather than hidden state that magically appears due to some hidden program flow.
- allochthon 4y ago
  I recently watched this intro to the topic, which I found really interesting: https://www.youtube.com/watch?v=bnnacleqg6k https://www.youtube.com/watch?v=bnnacleqg6k
  - mcdonje 4y ago
    That was a good talk. Thanks for linking it.
- josephcsible 4y ago
  > I've mostly favored procedural programming and only use objects when I have to because the abstraction can make the program harder to reason about, especially when there's a lot of inheritance. In functional programming, you generally abstract in different directions than you do in object-oriented programming. IMO, functional abstractions make things easier to reason about, since they generally constrain what any given block of code might do. > So, for someone who doesn't love objects, why should I love types? Because powerful type systems mean that a lot of mistakes will be compiler errors instead of bugs.
truth_seeker 4y ago
Recently I came across this fascinating live coding talk on Rust which focus on traits and structs to build extensible software APIs Type Driven API - https://www.youtube.com/watch?v=bnnacleqg6k https://www.youtube.com/watch?v=bnnacleqg6k Type level programming - https://willcrichton.net/notes/type-level-programming/ https://willcrichton.net/notes/type-level-programming/
jshaqaw 4y ago
A can’t miss awesome thing for people on the precipice of the dependent type theory rabbit hole is 1lab: https://1lab.dev/#lab https://1lab.dev/#lab 1lab is the future for mathematics research that deserves to happen.
- still_grokking 4y ago
  It's a pity I can't up-vote more than once. Really great resource! Thanks for sharing!
wellanyway 4y ago
...because Haskell isn't ivory enough anymore.

>"In Idris, types are first-class constructs in the langauge. This means types can be passed as arguments to functions, and returned from functions just like any other value, such as numbers, strings, or lists. This is a small but powerful idea, enabling: o Relationships to be expressed between values; for example, that two lists have the same length. o Assumptions to be made explicit and checked by the compiler. For example, if you assume that a list is non-empty, Idris can ensure this assumption always holds before the program is run. o If desired, properties of program behaviour to be formally stated and proven." PDS: I'd be curious to know about any/all languages where types can be passed to functions, returned from functions -- and even generated at runtime by functions... that is, where the language regards types as first-class constructs...

kitd 4y ago
This is presumably not what you're thinking of but ofc Javascript uses objects as prototype "types". As is, they wont provide what you want, but if there was some kind of "compile-time" processing of prototypes such that types assemblies, dependencies, constraints and other relationships could be manipulated or asserted before they were applied in runtime code, that may provide some of the "first-class type" functionality mentioned. Ed: actually, Typescript might be a better host for this.
- eckza 4y ago
  FP Or Die Gang is downvoting you, but this is actually correct. No referential transparency (among other things, no doubt) makes this a harder problem to solve than just using a language that supports it. $0.02
  - still_grokking 4y ago
    If you don't have referential transparency mathematical equations don't hold. You can't be sure that `a = b` stays true if deducted once. So "the problem" doesn't get only harder, it becomes impossible to solve in a formal way.
    - eckza 4y ago
      Thank you for this. That's exactly what I was getting at; you illustrated it far better.
- still_grokking 4y ago
  The down-votes are likely because the example isn't anyhow good. But the idea to have static prototype types is imho quite interesting on its own. I was thinking a lot about that in the past. I would love to have JS like objects—but in a static context. Row polymorphism and extensible records are close but still not there actually.
teddyh 4y ago
> PDS: I'd be curious to know about any/all languages where types can be passed to functions, returned from functions -- and even generated at runtime by functions... that is, where the language regards types as first-class constructs... Python does this.
- ihm 4y ago
  These types are statically checked (i.e., can be checked before runtime).
  - teddyh 4y ago
    I was not replying to the article, I was replying to the question from “peter_d_sherman” asking if any other programming language has types as first-class constructs. And Python does that.
    - peter_d_sherman 4y ago
      Sure! I'll accept Python into the list of languages that have types as first-class constructs! And thanks, the suggestion is much appreciated!
    - typedfalse 4y ago
      Eh, in this context those aren't types; instead Python is unityped. Agreed they are still fun though.
      - xigoi 4y ago
        Python is dynamically typed, but definitely not untyped.
        wk_end 4y ago
        typedfalse wrote "unityped", not "untyped" (note the "i"). When type system people talk about types they're implicitly talking about static types, rather than what Python might call a type. Robert Harper lays out the argument [0] that Python is basically a statically typed language with many "classes" but a single type - that's where I was first exposed to this idea. > The characteristics of a dynamic language are [that] values are classified [...] into a variety of forms that can be distinguished at run-time. A collection of values can be of a variety of classes, and we can sort out at run-time which is which and how to handle each form of value. Since every value in a dynamic language is classified in this manner, what we are doing is agglomerating all of the values of the language into a single, gigantic (perhaps even extensible) type. To borrow an apt description from Dana Scott, the so-called untyped (that is “dynamically typed”) languages are, in fact, unityped. Rather than have a variety of types from which to choose, there is but one! > And this is precisely what is wrong with dynamically typed languages: rather than affording the freedom to ignore types, they instead impose the bondage of restricting attention to a single type! Every single value has to be a value of that type, you have no choice! Even if in a particular situation we are absolutely certain that a particular value is, say, an integer, we have no choice but to regard it as a value of the “one true type” that is classified, not typed, as an integer. Conceptually, this is just rubbish, but it has serious, tangible penalties. For one, you are depriving yourself of the ability to state and enforce the invariant that the value at a particular program point must be an integer. For another, you are imposing a serious bit of run-time overhead to represent the class itself (a tag of some sort) and to check and remove and apply the class tag on the value each time it is used. [0] https://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-languages/ https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...
ihm 4y ago
The most famous ones off the top of my head: Coq, Agda, Lean, Idris, ATS. Here's a list: https://en.wikipedia.org/wiki/Category:Dependently_typed_languages https://en.wikipedia.org/wiki/Category:Dependently_typed_lan...
- peter_d_sherman 4y ago
  That (and pages like that) are what I was looking for! Thanks, much appreciated!
  - still_grokking 4y ago
    Scala is missing on that list (even it doesn't have "full dependent types" Match-Types are quite close).
- eggy 4y ago
  I tried ATS after finding Rust difficult. Zig is becoming my C replacement, and ATS is like a C++ replacement, although, I am using SPARK2014 now, but I am looking into ATS' contracts. There is no lack of PLs as a tool for whatever you may need to do nowadays. It's refreshing compared to 1970s to 1980s for me.
deleted 4y ago
[deleted]
csande17 4y ago
Zig is probably the closest you'll get to this in an imperative language. You can write functions that take types as arguments and return types, and that's how e.g. generic data structures are implemented.
- astrange 4y ago
  You can do that in Smalltalk descendants, if by types you mean metaclasses.
  - still_grokking 4y ago
    No, types are not runtime values! That's the whole point. That's why dependent types are so special (and complicated): You can use them as first class constructs without them being runtime values ever. Everything happens in the type checker. At runtime there are no types in proper static languages; things like Java / C# are actually quite dynamic in contrast; the dynamic nature was even part of the marketing of those languages back than. (Runtime) reflection is just dynamic typing…
    - astrange 4y ago
      "Runtime value" is an implementation detail. You could write an Idris interpreter. It'd be useful too. Why should your whole project fail to run just because one file that's not going to get used has a type error?
      - still_grokking 4y ago
        > "Runtime value" is an implementation detail. You could write an Idris interpreter. Sure. And such an interpreter would still not interpret types at runtime, as types are not (runtime) values. Only at type-checking time (which is of course a phase before the program actually runs / gets interpreted) you would do anything with the types. > It'd be useful too. Why should your whole project fail to run just because one file that's not going to get used has a type error? Whether that would be anyhow "useful" depends on the definition of "file usage". If there's any reference form the "used" parts of the program to the "unused file" you have a problem: A type error (in a language where "programs as proves" is a thing) means that you "proved" false. But form a "prove" of false you can "prove" anything! So you actually lost all proving power. Your program may now explode at runtime with arbitrary type errors anywhere. At that point your "static type system" becomes completely useless. (Of course, if nothing in your "unused file" is referenced anywhere in the "used" files, noting happens. But in this case that "unused file" isn't part of your program, so it's completely irrelevant what's inside anyway.)
skybrian 4y ago
Zig does some of this. Functions can be written that can be called at compile time or runtime, depending on which language features they use. Types can be computed and returned by functions in compile-time expressions. I don't know how expressive the types can get, though?
- Avshalom 4y ago
  I'm going to guess not very expressive. Zig refuses to have operator overloading because it might be used to call a function that's more expensive than you'd guess so the idea that they'd let types enforce all that much seems unlikely.
- still_grokking 4y ago
  You can pass "types" also around in C#… But in both cases that aren't types in the sens of type theory. In both cases those are just regular values (of type "Type"). In both cases you will be able to find those values with the help of a debugger. (The difference between Zig and C# being that in Zig those values are constructed during compilation and than mostly thrown away again whereas the "type" values are just regular runtime data on the CLR).
  - skybrian 4y ago
    The types created in compile-time code are just as "real" as the types you declare in source code. All types become values at compile time. When you write a compiler, the parser creates ordinary values, perhaps instances of a Type type. The type-checking code operates on these values to find errors according to the rules of type theory. Compile-time functions are a way of calling user-defined code in the compiler, much like a macro but saner, and they can create types that can be used in declarations, verified by the type checker, and used as input to the code generator. (Reflective use of runtime types in languages like C#, Java, or Go is different.)
    - still_grokking 4y ago
      Even you almost didn't say anything wrong here there is a key misunderstanding: The term "type theory", which I've used and to which I referred (and which you've picked up), is a technical term form math. Languages like C# or Zig are not based on type theory. What is called "types" in those languages has (mostly) no relation to type theory. Those "types" are (mostly) regular values when looked at them through the type theory lens.
cpurdy 4y ago
>I'd be curious to know about any/all languages where types can be passed to functions, returned from functions -- and even generated at runtime by functions... that is, where the language regards types as first-class constructs... Ecstasy (xtclang).
still_grokking 4y ago
The examples are completely out of context. > Relationships to be expressed between values; for example, that two lists have the same length. This can be also expressed in any language, even in unityped (a.k.a. "dynamic") ones. You don't need types for that at all… > Assumptions to be made explicit and checked by the compiler. This can be also expressed in any language, even in unityped (a.k.a. "dynamic") ones. In theory you don't need types for that at all. (Even types would be the current std. method to achieve that). > For example, if you assume that a list is non-empty, Idris can ensure this assumption always holds before the program is run. You can construct a NEL (NonEmptyList) in any language. That's trivial. You just need to enforce the usage of the right factory method for your list. > If desired, properties of program behaviour to be formally stated and proven. This has nothing to do with dependent types (directly). A language based on simply typed lambda calculus is "enough" to arrive at this property.
- dmytrish 4y ago
  Exactly, you can ship software in unityped languages. Still, how do you express even such a simple thing as a generic list type in simply typed lambda calculus? It's just that dependent types enable you to express any invariants statically, without actually running the code. > You can construct a NEL (NonEmptyList) in any language. That's trivial. That's true, with the caveat of: this invariant only exists in your head and hopefully docs. When it's encoded in a type, your compiler gets awareness of this invariant as well. Then it's able to do things that were impossible before, it can catch bugs that you would not (e.g. due the sheer amount of source code). Even though there are other approaches to software verification, types are the only one that got mainstream adoption so far.
  - still_grokking 4y ago
    Of course. But the examples given missed the point imho. All of the stated things don't need any type level machinery. You can just test things at runtime and be good. If you want to prove things at compile time that's a very different story. But than this needs to be explicitly stated in the examples.

jshaqaw 4y ago

I'm a big fan of this book for anyone interested in the topic: https://www.amazon.com/Gentle-Introduction-Dependent-Types-Idris/dp/1723139416/ref=sr_1_2?crid=1TAWAM306Z0NE&keywords=idris+book+types&qid=1674232196&sprefix=idris+book+types%2Caps%2C82&sr=8-2 https://www.amazon.com/Gentle-Introduction-Dependent-Types-I...

peter_d_sherman 4y ago
Looks highly interesting... Thanks for the suggestion!
gre 4y ago
Better link... https://leanpub.com/gidti https://leanpub.com/gidti
- CoastalCoder 4y ago
  Anyone know if there's a decent way to get a printed copy? Or barring that, can anyone suggest a good device on which to read it and jot notes, for someone who normally prefers printed books?
  - nerdponx 4y ago
    I bought a basic b&w two-sided laser printer in 2011 for this purpose, and it's served me extremely well over the years. You can then take the stack of pages to a store like Staples and they will bind it for you for a few dollars. I got the Brother HL-2270DW and I think they still make it. They even publish official Linux drivers for CUPS! Just make sure to get the extended toner cartridges (TN450), the regular ones are a ripoff.
    - Jtsummers 4y ago
      Staples and others will also print and bind PDFs you bring in. I've done this with purchased books, sometimes they get a bit picky but usually they'll just do it.
  - deleted 4y ago

ykonstant 4y ago

I am dabbling in the cousin language Lean right now, and it is very fun to use!

peter_d_sherman 4y ago
Some quick info for Lean: Homepage: https://leanprover.github.io/ https://leanprover.github.io/ Source: https://github.com/leanprover/lean4 https://github.com/leanprover/lean4 Wikipedia: https://en.wikipedia.org/wiki/Lean_(proof_assistant) https://en.wikipedia.org/wiki/Lean_(proof_assistant)
- agentultra 4y ago
  I also wrote a guide: https://agentultra.github.io/lean-4-hackers/ https://agentultra.github.io/lean-4-hackers/
  - still_grokking 4y ago
    LEAN's syntax looks really great. I wish Scala could take some inspiration. Scala's syntax is anyway quite similar already, but would need proper Unicode support and some other "tuning" like the `:=` and the `let monadic ← effect` syntax, imho.
daxfohl 4y ago
One difference I see is Lean uses type classes while Idris uses implicits. Can anyone comment on the pros and cons of that decision? (Or pros and cons between the two languages in general?) It also seems that Idris was created as a general-purpose language first, whereas Lean started as a proof assistant and only recently added general-purpose language. Is that evident when using the languages? A quick look at Lean's general-purpose language seems reasonably similar to the Indris experience AFAICT.
- ImprobableTruth 4y ago
  Imo the biggest difference is the "heritage", Lean is Coq inspired, Idris Agda inspired. This manifests in how people prove things. Idris has dependent pattern matching, so proofs are written as normal terms. Lean has tactics and proofs are small tactics scripts (which then generate the proof term behind the scene). Other than that, the difference is mainly in infrastructure/libraries and community.

peter_d_sherman 4y ago

There also seems to be some intersection here between type-driven development and Proof Assistants: https://en.wikipedia.org/wiki/Proof_assistant https://en.wikipedia.org/wiki/Proof_assistant

jshaqaw 4y ago
A huge overlap. Idris is aimed at being a general purpose language with proof assistant characteristics while some of its peers are more theorem provers built with general purpose language characteristics.
chills 4y ago
See also: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- peter_d_sherman 4y ago
  Wowzer! That is quite the page... There is definitely something there! That page is decidedly worth reading and re-reading many times in the future... I think it boils down to the following: >"Curry–Howard correspondence [...] is the direct relationship between computer programs and mathematical proofs." And: >"If one abstracts on the peculiarities of either formalism, the following generalization arises: a proof is a program, and the formula it proves is the type for the program." In fact, I'm going to go for "full crackpot" here... If all computer programs are algorithms, and all mathematical proofs are algorithms, and all types are algorithms -- then a "grand unifying theory" between Computer Programs and Mathematics -- looks like this: It's all Algorithms. Algorithms on top of algorithms. You know, like turtles on top of turtles... This makes sense too, if we think about it... Algorithms are just series of steps, with given inputs and given outputs. That is no different than Computer Programs. And that is no different than Math... You can call this series of steps an Algorithm, you can call it a Function, you can call it y=f(x), you can call it a Type, you can call it a Computer Program, you can call it a Math Equation, you can call it a logical proposition, and you can use whatever notation and nomenclature you like -- but in the end, in the end, it all boils down to an Algorithm... A series of steps... Now, perhaps that series of steps -- uses other series of steps -- perhaps that Algorithm uses other Algorithms, perhaps that function uses other functions, perhaps that Computer Program uses other computer programs, perhaps that Math Equation uses other math equations, etc., etc. -- But in the end, in the end... It's all a series of rigorously defined steps... It's all an Algorithm... Or Algorithm consisting of other Algorithms... (recursively...) Patterns of steps -- inside of patterns of other steps (again, recursively...) Anyway, great page, definitely worth reading and re-reading!

nightowl_games 4y ago

Anyone else finding this documentation is pretty hard to navigate? Makes me think this isn't a serious language, but rather an academic toy or resume builder.

andrewmcwatters 4y ago
The main repository is in the top 1% of stargazed repositories on GitHub, and the project has a mailing list, Discord server, IRC, AND Slack. It has been forked over 300 times, and has over 100 contributors. What in the world counts as "serious" to some of you people? Sometimes I read HN and ask myself if people here know at all how hard it is make something people want, and how many people know what the real-world thresholds are for understanding when you have made something that people want. I guess if everyone hasn't heard of it, people here don't think it's serious.
- bobleeswagger 4y ago
  [flagged]
  - andrewmcwatters 4y ago
    I mean you tell me, which would be bullying to you? You work for years on something and someone tells you it's not "serious" because they haven't learned to browse a source tree, or the guy telling him to read a little more? Either way, I apologize for how it came off.
    - bobleeswagger 4y ago
      > someone tells you it's not "serious" because they haven't learned to browse a source tree "Fuck this stranger for not learning something I know how to do!"
- mejutoco 4y ago
  I find Idris incredibly interesting. Specially combined with the output it can generate in other languages. The book of it is also a masterpiece, even if you never program in it. Already lots of "serious" hacked together programming languages. The only downside I see if the lack of a package manager.

satvikpendem 4y ago

The book itself Type Driven Development with Idris is great too, it is the principal way I write code these days, by writing my types upfront then filling out the logic, and in some languages, the logic itself can be produced automatically via the filling of type holes. In other words, simply based on the types you provide, the compiler can guess the implementation of the function, somewhat like Copilot but guaranteed to be correct on a type level, even if not necessarily on a business logic level. https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...

acchow 4y ago
I had never heard of this book before, now I definitely want to give it a try. As an aside, isn't type driven development how everyone codes naturally in statically typed languages? Whether it's Ocaml or Java, I feel like I try to get the types defined, then put on music and turn my brain off and just line the types up (much moreso in Ocaml than in Java).
- satvikpendem 4y ago
  Indeed, and this is precisely why I hate writing in dynamically typed languages like Ruby or Python; they hinder me from thinking about the shape of the program clearly.
  - iddan 4y ago
    Well now you can write full types in both of them
    - shpongled 4y ago
      You can write them, but without most of the benefits of static types
      - mejutoco 4y ago
        You can typecheck them with mypy or pyright or at runtime with typeguard. It is not ideal, but pretty good in terms of benefits.

spelunker 4y ago

Here's an intro to dependent types from David Christiansen, I think it came up during another dependent types discussion: https://youtu.be/VxINoKFm-S4 https://youtu.be/VxINoKFm-S4

theresistor 4y ago

What's the state of Idris2 at this point? I really enjoyed Type Driven Development with Idris a few years ago.

still_grokking 4y ago
It's the current version. https://www.idris-lang.org/idris-2-version-060-released.html https://www.idris-lang.org/idris-2-version-060-released.html Idris 1 seems obsolete since years. No news about it for a long time. https://www.idris-lang.org/category/news.html https://www.idris-lang.org/category/news.html

mcdonje 4y ago

I know I'm missing something, but this seems like the functional version of object classes. I've mostly favored procedural programming and only use objects when I have to because the abstraction can make the program harder to reason about, especially when there's a lot of inheritance. But I've heard some hype about types in Rust, and now this. The free chapter in the manning book even introduces types in terms of real world objects. So, for someone who doesn't love objects, why should I love types?

ok_dad 4y ago
Where objects can hide state or I/O in a program, types and functional type driven development make each function very clear as to what it has for input and outputs and part of that is not hiding state anywhere that doesn’t make sense. You might still have a global logger because that makes sense, but generally you know the things you have access to because they’re in the function signature. It can break down if you aren’t careful, and there’s some nuance where you might still store a configuration data as an object property, but it’s a clearly typed property that’s assigned at initialization rather than hidden state that magically appears due to some hidden program flow.
allochthon 4y ago
I recently watched this intro to the topic, which I found really interesting: https://www.youtube.com/watch?v=bnnacleqg6k https://www.youtube.com/watch?v=bnnacleqg6k
- mcdonje 4y ago
  That was a good talk. Thanks for linking it.
josephcsible 4y ago
> I've mostly favored procedural programming and only use objects when I have to because the abstraction can make the program harder to reason about, especially when there's a lot of inheritance. In functional programming, you generally abstract in different directions than you do in object-oriented programming. IMO, functional abstractions make things easier to reason about, since they generally constrain what any given block of code might do. > So, for someone who doesn't love objects, why should I love types? Because powerful type systems mean that a lot of mistakes will be compiler errors instead of bugs.

truth_seeker 4y ago

Recently I came across this fascinating live coding talk on Rust which focus on traits and structs to build extensible software APIs Type Driven API - https://www.youtube.com/watch?v=bnnacleqg6k https://www.youtube.com/watch?v=bnnacleqg6k Type level programming - https://willcrichton.net/notes/type-level-programming/ https://willcrichton.net/notes/type-level-programming/

jshaqaw 4y ago

A can’t miss awesome thing for people on the precipice of the dependent type theory rabbit hole is 1lab: https://1lab.dev/#lab https://1lab.dev/#lab 1lab is the future for mathematics research that deserves to happen.

still_grokking 4y ago
It's a pity I can't up-vote more than once. Really great resource! Thanks for sharing!

wellanyway 4y ago

...because Haskell isn't ivory enough anymore.