![[Home]](http://www.bayleshanks.com/cartoonbayle.png)
https://gist.github.com/graninas/22ab535d2913311e47a742c70f1d2f2b/c4e1b25cefe673a0c1d1bec4c24690121f31fa21 describes Rust as "Haskell without HKTs"
https://typelevel.org/blog/2016/08/21/hkts-moving-forward.html says of higher-kinded types "However, there is a point of inflection in the book at chapter 11. You can pass through with a language such as OCaml, Scala, Haskell, PureScript?, or one of a few others. However, users of Java, C#, F#, Elm, and many others may proceed no further, and must turn back here."
https://medium.com/@patxi/intro-to-higher-kinded-types-in-haskell-df6b719e7a69 gives examples of higher-kinded types:
" A List<T> in Java is a list that contains things of T type.... ... For types that do not construct other types, the kind is said to be *. In the case of a list, kind is * -> * (following the arrow you can understand that when you give a type, you get another one). ... But... can you define in Java something like any container type holding a String? This should be like generics but reversed: if this were possible, it could be expressed as T<String>. In Haskell this is represented as a String (“a” is just an arbitrary name as “T” in Java). ... Let’s see this in detail by an example in Haskell.
Imagine that we have a User data type:
data User = User { name :: String , age :: Int }
and a function that receives a given user name and returns a Maybe of User:
userByName :: String -> Maybe User userByName name
| name == “haskell” = Just (User name 29) |
| otherwise = Nothing |
So now we are going to define a new function which will receive a String and then look for an optional User and return its age in case the user exists. This function will basically use the previous one and then obtain user’s age if it exists. We could think on doing this:
ageForUser :: String -> Maybe Int ageForUser name = fmap age (userByName name)
This works and it’s fine, we fmap the content of the result of calling userByName function using the age function to get user’s age (fmap function is available as Maybe has an instance of the Functor type class). But this function is needlessly coupled to Maybe. Does this function really need to know about it?
We want to have something like this:
ageForUser :: String -> a Int ageForUser name = fmap age (userByName name)
But this will not compile, here we are trying to tell the compiler: given a String parameter, we want to return a Maybe String in our particular case (a will be the Maybe “hole”). But we cannot define the function this way as the function return type is open for every type whose kind is * -> *. A client of this function will not have any way to know the concrete type, that’s why the compiler even does not allow us doing it. In some way the function type signature does not meet referential transparency (at type level).
...
ageForUser :: Functor a => String -> (String -> a User) -> a Int ageForUser name userFinder = fmap age (userFinder name)
"
---
" Maps are open
The other interesting thing about specs for maps is that they are open. For example, if we use the same exact map as before, with the same fields and an additional field called ::age, it's still a valid ::user:
...
On the other hand, a lot of people who use spec to validate things coming from outside their system need to be more strict with maps, and they have complained about the openness of maps. We'll talk about proposed solutions to this issue later. " -- https://www.pixelated-noise.com/blog/2020/09/10/what-spec-is/
---
"
Sequence specs - regular expressions for data
A powerful mechanism in spec is sequences. We've already seen s/coll-of which contains a uniform type of values (a collection of numbers for example) but sequences are a bit more like regular expressions for data. In this case we have a sequence with two things, which describe an ingredient for a recipe: the first thing is a number for the quantity and the second thing is a unit encoded as a keyword.
(require '[clojure.spec.alpha :as s])
(s/def ::ingredient (s/cat :quantity number? :unit keyword?))
With s/cat we always have to give a name to each position. s/cat allows to both validate the shape of the value passed, but it also enables the "conform" operation, which is somehow similar to parsing or destructuring. If we pass a vector of two elements – a number and a keyword – we get back a map with the defined names:
(prn (s/conform ::ingredient [2 :teaspoon]))
{:quantity 2, :unit :teaspoon}
By using some of the other operators which are reminiscent of regular expressions, this technique can become quite powerful. As an example, we'll try and create a very simple grammar that can parse a very limited subset of the Clojure syntax. Specifically, we will attempt to parse defn, which is the macto used to define functions. The s-expression includes defn as a symbol, then a symbol that defines the name of the function, then an optional docstring (a string), a vector of the arguments, and finally the function body.
Let's express this as a cat spec:
(require '[clojure.spec.alpha :as s] '[clojure.pprint :as pp])
(s/def ::function (s/cat :defn #{'defn} :name symbol? :doc (s/? string?) :args vector? :body (s/+ list?)))
So this is how what our spec looks like: there is a defn part, which is always the symbol defn. We use a set as the predicate, so a value passes if it's contained in the set. Then we have :name which is a symbol. Next we have s/? for the docstring which means that there can be zero or one strings in that position. After that we have the argument which is a vector (with undefined contents to keep things simple), and finally a list to hold the function's body.
We can try our spec on some data that looks like a valid Clojure function (remember, we're in a Lisp, so code is data is code!):
(def function-code1 '(defn my-function "this is a test function" [x y] (+ x y)))
(pp/pprint (s/conform ::function function-code1))
{:defn defn, :name my-function, :doc "this is a test function", :args [x y], :body [(+ x y)]}
The different parts are properly identified. Now let's try conforming the same function but without the docstring:
(def function-code2 '(defn my-function [x y] (+ x y)))
(pp/pprint (s/conform ::function function-code2))
{:defn defn, :name my-function, :args [x y], :body [(+ x y)]}
Again, the different parts are properly identified.
This opens up a lot of possibilities for DSLs, for validating macros etc and it's generally a very powerful technique. This kind of code to handle optional values in the middle of a sequence is tricky to write in a functional way, so conform helps a lot. Generate data
Spec is a declarative skeleton made of up s/keys, s/cat, s/+, s/* etc and right at the bottom there are predicates.
...
Access data with lenses
The other pattern that has proven very useful for me and was enabled by spec is a way to access or modify deeply nested data structures (sometimes called "lenses") and having this access checked by spec. I have released this as a little library called spectacles.
So let's have a look at this spec which is a little bit more complex in that it describes a data structure with a bit of depth. We have a top-level spec, which has two keys, :filename and :target-dims, and we also have a value that conforms to the spec:
(ns my-ns (:require [spectacles.lenses :as lens] [clojure.spec.alpha :as s]))
(s/def ::filename string?) (s/def ::dims (s/coll-of string?)) (s/def ::target-dims (s/keys :req-un [::dims] :opt-un [::the-cat])) (s/def ::the-cat (s/cat :a string? :b number?)) (s/def ::top (s/keys :req-un [::filename ::target-dims]))
(def top {:filename "foo" :target-dims {:dims ["foo" "bar"]}})
We then call lens/get with 3 parameters: the data structure, the spec that describes it and the key to get:
(lens/get top ::top :filename)
"foo"
...
No metadata (yet): Another problem is that there are facilities for adding metadata to specs: for example you can't attach a docstring to a spec (although the criticism of this is that a spec IS documentation, why would you document the documentation?). Metadata would be useful in other cases too: you could attach metadata that would help you generate the API of your server. " -- https://www.pixelated-noise.com/blog/2020/09/10/what-spec-is/
" gw 2 days ago [–]
I think the instrumenting and generator stuff gets disproportionate attention. For me by far the biggest win from spec has been with parsing. This completely changes how you'd write a library that takes a data structure and parses it into something meaningful (for example, what hiccup does for html or what honeysql does for sql).
In the past, this required a lot of very ugly parsing code and manual error-checking. With spec, you write specs and call s/conform. If it failed, you get a nice error, especially if you pair it with expound. If it succeeded, you get a destructured value that is really easy to pull data out of. I've done this in a half dozen different libraries and i'm pretty sure i wouldn't have even written them without spec.
reply
tekacs 2 days ago [–]
As a very heavy user of spec, I’ve since switched to using Malli [0], which is similar but uses plain data to model specs (and doesn’t use Clojure Spec at all).
Also, Malli is being funded / supported by Clojurists Together [1], which is a wonderful initiative that’s also worth a look.
[0]: https://github.com/metosin/malli
[1]: https://www.clojuriststogether.org/news/q3-2020-funding-anno...
reply
" -- https://news.ycombinator.com/item?id=24432461
jwr 2 days ago [–]
I found spec very useful and use it more and more. I'm looking forward to newer revisions, with support for optionality, it's been a big problem area in my case.
Here's a quick list of gotchas (well, they got me, so perhaps other people will find this list useful):
The naming of `s/valid?` suggests that you can call it on your data and find out if the data is valid according to the spec. This isn't true. What it actually tells you is if the data, when conformed, will be valid according to the spec. If you pass the data as-is to your functions (without passing it through `s/conform`), you might find that they will be surprised at what they get.
I settled on a subset of spec, because of the pitfalls.
reply
didibus 2 days ago [–]
I think all of those problems are only true when you try to do coercion with custom conformers. Which is not the intended use of conformers.
Conformers are meant to parse the data when there are multiple possibility of what something can validate against, the conformer will disambiguate and return a result that tells you which path was chosen.
Coercion is not supported as part of Spec, you're expected to do that seperatly either before or after validating/conforming.
reply
jwr 2 days ago [–]
Yes, that was largely my point. Many people (me included) assume that s/conform is a kind of coercion, which it is not.
Not all of the above problems are due to coercion, but the majority are.
To be clear: I'm not complaining here, I find spec to be very useful and I like it, just pointing out traps for the unwary.
reply
hospadar 2 days ago [–]
We use spec A LOT to validate a huge config file/DSL thing for our internal ETL application.
My general feelings are:
reply
--- already copied to plbook:
unsound type system in Dart v1 but not in v2
" You can design a type system that's simple, sound, and expressive. But you only get to pick two of those adjectives. Today, because programmers are delightfully spoiled by a wealth of nice, expressive type systems, I think they won't settle for simple and sound.
Dart tried simple and expressive, but the lack of soundness made tooling much harder and really confused users who felt like they were being sufficiently penitent in their type annotations but still got punished for the sins of unsoundness anyway — type failures that were only caught at runtime.
So I think if you're designing a type system for a language today, you end up pushed pretty hard towards "sound + expressive", but now you're talking about a really complex beast. " -- [1]
my note:
---
what does Haskell do about all that? Nothing: Haskell doesn't even have subtyping. Well, wait, it has typeclasses. Hmm, i'll have to think about it more when i have time.
---
i guess my feeling about the previous section is that we should just have generics, local type inference, and the proper variances, plus a 'dynamic' escape hatch (or rather.. dynamic by default, and the option of static typing with the proper variances).
Need to think about what Haskell does about all this sometime.
---
doesn't look particularly relevant, but you never know:
https://www.fpcomplete.com/blog/2016/11/covariance-contravariance/
---
The AbsCell? class has an abstract type member T and an abstract value member init. Instances of that class can be created by implementing these abstract members with concrete definitions.
val cell = new AbsCell? { type T = Int; val init = 1 } cell.set(cell.get * 2)
The type of cell is AbsCell? { type T = Int }.
Path-dependent Types: You can also use AbsCell? without knowing the specific cell type:
def reset(c: AbsCell?): Unit = c.set(c.init);
Why does this work?
In general, such a type has the form x0...xn.t, where
---
" Scala's implicits are its most distinguished feature. They are the fundamental way to abstract over context. They represent a unified paradigm with a great variety of use cases, among them: implementing type classes, establishing context, dependency injection, expressing capabilities, computing new types and proving relationships between them.
Following Haskell, Scala was the second popular language to have some form of implicits. Other languages have followed suit. E.g Rust's traits or Swift's protocol extensions. Design proposals are also on the table for Kotlin as compile time dependency resolution, for C# as Shapes and Extensions or for F# as Traits. Implicits are also a common feature of theorem provers such as Coq or Agda.
Even though these designs use widely different terminology, they are all variants of the core idea of term inference. Given a type, the compiler synthesizes a "canonical" term that has that type. Scala embodies the idea in a purer form than most other languages: An implicit parameter directly leads to an inferred argument term that could also be written down explicitly. By contrast, type class based designs are less direct since they hide term inference behind some form of type classification and do not offer the option of writing the inferred quantities (typically, dictionaries) explicitly.
Given that term inference is where the industry is heading, and given that Scala has it in a very pure form, how come implicits are not more popular? In fact, it's fair to say that implicits are at the same time Scala's most distinguished and most controversial feature. I believe this is due to a number of aspects that together make implicits harder to learn than necessary and also make it harder to prevent abuses. ... Being very powerful, implicits are easily over-used and mis-used. This observation holds in almost all cases when we talk about implicit conversions, which, even though conceptually different, share the same syntax with other implicit definitions ... .
Another widespread abuse is over-reliance on implicit imports. This often leads to inscrutable type errors that go away with the right import incantation, leaving a feeling of frustration. Conversely, it is hard to see what implicits a program uses since implicits can hide anywhere in a long list of imports.
The syntax of implicit definitions is too minimal. It consists of a single modifier, implicit, that can be attached to a large number of language constructs. A problem with this for newcomers is that it conveys mechanism instead of intent. For instance, a type class instance is an implicit object or val if unconditional and an implicit def with implicit parameters referring to some class if conditional. This describes precisely what the implicit definitions translate to -- just drop the implicit modifier, and that's it! But the cues that define intent are rather indirect and can be easily misread, as demonstrated by the definitions of i1 and i2 above. ...
Existing Scala programmers by and large have gotten used to the status quo and see little need for change. But for newcomers this status quo presents a big hurdle. I believe if we want to overcome that hurdle, we should take a step back and allow ourselves to consider a radically new design. The New Design
The following pages introduce a redesign of contextual abstractions in Scala. They introduce four fundamental changes:
Given Instances are a new way to define basic terms that can be synthesized. They replace implicit definitions. The core principle of the proposal is that, rather than mixing the implicit modifier with a large number of features, we have a single way to define terms that can be synthesized for types.
Using Clauses are a new syntax for implicit parameters and their arguments. It unambiguously aligns parameters and arguments, solving a number of language warts. It also allows us to have several using clauses in a definition.
"Given" Imports are a new class of import selectors that specifically import givens and nothing else.
Implicit Conversions are now expressed as given instances of a standard Conversion class. All other forms of implicit conversions will be phased out.... Overall, the new design achieves a better separation of term inference from the rest of the language: There is a single way to define givens instead of a multitude of forms all taking an implicit modifier. There is a single way to introduce implicit parameters and arguments instead of conflating implicit with normal arguments. There is a separate way to import givens that does not allow them to hide in a sea of normal imports. And there is a single way to define an implicit conversion which is clearly marked as such and does not require special syntax.This design thus avoids feature interactions and makes the language more consistent and orthogonal. It will make implicits easier to learn and harder to abuse. It will greatly improve the clarity of the 95% of Scala programs that use implicits. It has thus the potential to fulfil the promise of term inference in a principled way that is also accessible and friendly. " -- https://dotty.epfl.ch/docs/reference/contextual/motivation.html
"
Implicit
The implicit keyword is one of my least favourite Scala language constructs. Take implicit parameters for example. It used to be you would have functions, and they would take arguments. To be able to drop some of the arguments for whatever reason, you could partially apply the function with the arguments you want to leave off. Java’s typically verbose version is to have a class reference it’s own instance fields in a method (watch the functional weenies writhe in agony over that comparison). Alternatively you could create a function which closed over a variable in scope. Now Scala allows you to have an implicit parameter, which means somewhere in the code there can be a declaration that says “if you’re looking for something of type Foo to pass to some method, use me”. Then when you invoke the method, if you have that declaration in scope, you don’t have to actually reference it to pass it to the method, Scala’s compiler will look it up for you.
So what’s my problem? For me, that lookup is opaque, it hides the parameter, kinda like bunging it in a ThreadLocal? and referencing it further down the call stack. It’s more difficult to keep the data flow in your head than it needs to be, and it’s pointlessly different from passing an argument to a function. Are there use cases for it? Probably, likely some pretty good ones somewhere. I’m told that the implicit CanBuildFrom? parameter in the Scala Collections library is solving problems that can’t be solved any other way. So fine, I make my peace with the guts of a library doing using implicit parameters, as long as it hides the complexity from me. For those implicit parameters that bleed out into an API, have any of the uses of I’ve come across been good? No, not yet. Has every example I’ve seen been a hindrance to readability? Yes.
Conversions are Scala’s other use of implicit. If a method takes a type Foo, and you try to pass in Bar, before the compiler tells you to fix your obvious type error, it first tries to discover if there’s a way to convert a Bar to a Foo and use that instead. Similarly if you try to invoke a method on Foo that doesn’t exist: before raising an error the compiler will look around for any available conversion that can turn Foo into something with a matching method.
So what’s my problem? Similar to implicit parameters, it’s the opaque, hidden lookup that detracts from readability. The bit where implicit conversions kinda sorta look like a really neat composition syntax (this type Bar is really just a Foo with an extra method or two) is really enticing. The “Enrich My Library” pattern is a really useful concept, but it’s the easy composition bit that does the legwork, I can’t help but think that’s where the feature should have ended, the use of implicit ruins it for me.
One argument I’ve seen in favour of Scala’s implicit conversions is that “Java also has these conversions, like from int to long, Scala just makes it available”. Correct: Scala does make it available. Instead of needing to learn a handful of weird, edge-case ridden, confusing conversions in Java, you have to learn every Tom, Dick and Sally’s weird, edge-case ridden, confusion conversion they’ve added to their library. And boy do people who like to experiment with new languages like to take that availability and run with it. And they run right past it’s logical conclusion End Zone. They run through that End Zone like Forrest Gump. Except when they keep running, they cease to be Forrest Gump, they’re actually Arnold Schwarzeneger, and are now being violently hunted down in a game show format, because the compiler found “implicit def toRunningMan()” in scope.
If you think that makes no sense, try debugging an accidentally and silently “missed” implicit conversion in ScalaQuery’s? DSL. " -- [4]
---
example of scala 3 'givens' which are (part of) the successor to scala implicits:
https://alvinalexander.com/source-code/scala-3-dotty-complete-givens-using-example/
so afaict these are just similar to Haskell typeclass instances. I guess what scala is really contributing is that i think these are lexically scoped, rather than globals like (i think) in Haskell.
---
so i get a sense from the previous two sections that something that is important in Scala land is implicits, and their most important use case is being replaced by givens, and givens are similar to typeclasses/typeclass instances. So this just strengthens my belief that everything-is-a-typeclass is important for Oot.
---
"The key differentiators between the type systems I didn’t value and those I now do — between thinking all type systems were worthless and thinking a good type system is worth its weight in gold — were: Type inference ... Sum/tagged union types: because a great many of the problems we solve in software come down to well-defined options: A or B or C, and with discrete options for what data goes with each of A and B and C....The fact that languages with first-class support for sum types also come with exhaustiveness checking for those was the icing on the cake. ... Soundness: I was sick to death of null and NullPointerException? and undefined is not a function and TypeError?: object of type 'NoneType?' has no len()....Getting them in a language with types was utterly infuriating: why couldn’t the compiler tell me that I had missed a case where something could be null?...Soundness changed all of that. It didn’t mean I was free from logic bugs. " -- https://v5.chriskrycho.com/journal/things-i-was-wrong-about/1-types/
---
https://docs.racket-lang.org/ts-reference/index.html
---
pjmlp 8 hours ago
| unvote [–] |
I predict that GC languages will prevail and adopt affine types for advanced users to code application hot paths, like D, Swift, Chapel among others are pursuing.
reply
throwaway17_17 8 hours ago [–]
I think this is in general the right call, but I would prefer seeing the adoption of a more general substructural type system implementation and the inclusion of uniqueness types. It would not add that much complexity when the use case is specifically limited to advanced users and the obvious trade offs in syntax increase and annotations are limited to those that want/need it.
reply
---
"minimal const generics":
https://without.boats/blog/shipping-const-generics/
https://internals.rust-lang.org/t/stabilizing-a-const-generics-mvp/12727
https://github.com/rust-lang/compiler-team/issues/332
from https://github.com/rust-lang/lang-team/issues/37 and https://github.com/rust-lang/rust/issues/74878
---
different types of abs date times (dates, times, times with various precisions) have some sort of relationship to each other. a typeclass? feels more like units. in32 and int64 are related in the same way. what about int and floats (subset/projections?). and all precision jnts are subsets of arbitrary precision/mathematical ints. autopromotion/coercion?
---
Julia: dynamism and performance reconciled by design section 4.1 describes some aspects of Julia's type system, and references Julia Subtyping: A Rational Reconstruction for more detail.
---
"
Again, many types get methods like expr.is_constant().
if some_condition && expr.is_constant() { ... }
In zig:
if (some_condition and expr == .Constant) { ... }
This works because tagged unions in zig create a separate type for the tag itself and there is an implicit cast from the union to the tag. " -- [5]
---
" Zig has no syntax for closures. You can create closures manually, but it's verbose. There is a tracking issue open but it doesn't look like there is a consensus yet. The lack of closures limits some kinds of apis eg a direct port of differential dataflow to zig would be unpleasant to use.
Zig has no equivalent to smart pointers. I haven't wanted any yet, but I expect to miss rust's Rc eventually. Manually incrementing reference counts is hilariously error-prone. " -- [6]
---
" Zig has various implicit casts that it will make whenever a value of one type is stored in a slot of another type.
For example, there is a cast from anonymous lists to arrays, and from a pointer to an array to a slice.
const a: [3]usize = .{0, 1, 2}; const b: []const usize = &a;
But zig won't chain these casts, so you can't directly cast an anonymous list to a slice.
const c: []const usize = &.{0,1,2};
./test.zig:62:32: error: expected type '[]const usize', found '*const struct:62:33' const c: []const usize = &.{0,1,2};
To do this in one line requires the full explicit syntax:
&[_]usize{0,1,2};
The equivalent is rust is:
&[0,1,2];
A minor papercut to be sure, but slice literals are everywhere. " -- [7]
---
https://www.cl.cam.ac.uk/~jdy22/papers/effective-concurrency-through-algebraic-effects.pdf
some ppl including Leo White of Ocaml's take on algebraic effects
looks good. Short paper.
---
glouwbug 1 day ago [–]
If anyone is interested, I'm in the process of back porting the STL to C99: https://github.com/glouw/ctl
The gist of its workings is including a header and defining its type:
For more complex types, copy, free, and default constructors are supported, given they're defined before the inclusion of the container:
typedef struct { void* data; } blob;
blob blob_copy(blob* self) { ... } // Copy constructor
void blob_free(blob* self) { ... } // Destructor
blob blob_init(void* data) { ... } // Constructor
blob blob_init_default(void) { ... } // Default constructor
#define T blob
#include <vec.h> int main(void)
{
vec_blob blobs = vec_blob_init();
vec_bloc_push_back(&blobs, blob_init(...)); // Invokes constructor, element 0, passed by value
vec_blob_resize(&blobs, 42); // Invokes default constructor for elements 1-42.
vec_blob copy = vec_blob_copy(&blobs); // Invokes copy constructor for elements 0-42.
vec_blob_free(&blobs); // Invokes destructor for elements 0-42.
vec_blob_free(©);
}The motivation for starting this project was to provide C++ like functionality to C, but provide hugely reduced build times.
reply
---
ido 1 day ago [–]
As someone who rarely ever used c++ (and without templates when I did), what do they give you vs Generics like c# or java?
reply
giomasce 21 hours ago [–]
Not GP and I know some Java, but not C#. As I get it, in Java generics are little more than sugar coating: they basically check that your are not messing up with types. Having a List<String> is not very different (maybe not at all) from having a List<Object> and casting elements between Object and String when you put or get them, except that the compiler can check the types at compilation time. The List code is essentially the same.
By contract, a std::vector<std::string> and a std::vector<int> in C++ are two completely different and unrelated classes. Any code they used is compiled twice, once for every value of the template parameter, and of course is optimized independently in each case. So, for example, although the template code is the same, the operation of copying a vector an give very different assembly codes: copying a vector of strings requires to call the copy constructor of each single string in the new vector, but copying a vector of ints basically reduces to calling memcpy() appropriately (thanks to all the appropriate abstractions, so that the compiler knows that to copy an int it is enough to copy its bytes, and this cannot fail due to an exception, and maybe other things).
This is one of the great thing in C++ (at least, if you value this kind of optimizations), and it seems that OP misses the point entirely. It gives what is called (when it works) "zero-cost abstraction". You might like it or not, but it makes no sense to judge C++ design choices if you don't consider the ability to do zero-cost abstraction (which, for example, Java does not have).
reply
---
" Thus it is actually useful to clarify all the things Zig doesn’t have to show how small it is:
No class inheritance like in C++, Java, Swift etc.
No runtime polymorphism through interfaces like Go.
No generics. You cannot specify generic interfaces like in Swift checked at compile time.
No function overloading. You cannot write a function with the same name multiple times taking different arguments.
No exception throwing.
No closures.
No garbage collection.
No constructors and destructors for use with Resource acquisition is initialization (RAII).However Zig is able to provide much the same functionality by clever use of a few core features:
Types can be passed around like objects at compile time.
Tagged Unions. Also called sum types or variants in other programming languages.
Function pointers.
Real pointers and pointer arithmetic.
Zig code can be partially evaluated at compile time. You can mark code to be executable at compile time, with comptime keyword.
Functions and types can be associated with structs, but are not physically stored in structs, so invisible to C code." [8]---
Zig-like 'comptime', with 'const's and type values that only exist at compile time
some examples in https://web.archive.org/web/20201111014207/https://erik-engheim.medium.com/is-zig-the-long-awaited-c-replacement-c8eeace1e692
---
on Jai: "Its templates are not that different from C++. The syntax is much improved; C++ chose a very clunky syntax solely so that it wouldn't conflict with C. It also doesn't have SFINAE, which makes debugging compiler errors much easier, since it doesn't have to do a backtracking search to find the correct template instance. This also makes template resolution faster."
---
" String literal types in TypeScript? allow us to model functions and APIs that expect a set of specific strings.
function setVerticalAlignment(pos: "top"
| "middle" | "bottom") { |
// ...}
setVerticalAlignment("middel"); ~~~~~~~~ error: Argument of type '"middel"' is not assignable to parameter of type '"top"
| "middle" | "bottom"'. |
This is pretty nice because string literal types can basically spell-check our string values.
We also like that string literals can be used as property names in mapped types. In this sense, they’re also usable as building blocks.
type Options = { [K in "noImplicitAny"
| "strictNullChecks" | "strictFunctionTypes"]?: boolean |
---
this sounds too powerful for me:
" Recursive Conditional Types
In JavaScript? it’s fairly common to see functions that can flatten and build up container types at arbitrary levels. For example, consider the .then() method on instances of Promise. .then(...) unwraps each promise until it finds a value that’s not “promise-like”, and passes that value to a callback. There’s also a relatively new flat method on Arrays that can take a depth of how deep to flatten.
Expressing this in TypeScript’s? type system was, for all practical intents and purposes, not possible. While there were hacks to achieve this, the types ended up looking very unreasonable.
That’s why TypeScript? 4.1 eases some restrictions on conditional types – so that they can model these patterns. In TypeScript? 4.1, conditional types can now immediately reference themselves within their branches, making it easier to write recursive type aliases.
For example, if we wanted to write a type to get the element types of nested arrays, we could write the following deepFlatten type.
type ElementType?<T> = T extends ReadonlyArray?<infer U> ? ElementType? : T;
function deepFlatten<T extends readonly unknown[]>(x: T): ElementType?<T>[] { throw "not implemented"; }
All of these return the type 'number[]': deepFlatten([1, 2, 3]); deepFlatten([[1], [2, 3]]); deepFlatten([[1], [[2?]], [[[3?]]]]);
Similarly, in TypeScript? 4.1 we can write an Awaited type to deeply unwrap Promises.
type Awaited<T> = T extends PromiseLike?<infer U> ? Awaited : T;
/ Like `promise.then(...)`, but more accurate in types. declare function customThen<T, U>( p: Promise<T>, onFulfilled: (value: Awaited<T>) => U ): Promise<Awaited>;
Keep in mind that while these recursive types are powerful, but they should be used responsibly and sparingly.
First off, these types can do a lot of work which means that they can increase type-checking time. Trying to model numbers in the Collatz conjecture or Fibonacci sequence might be fun, but don’t ship that in .d.ts files on npm.
But apart from being computationally intensive, these types can hit an internal recursion depth limit on sufficiently-complex inputs. When that recursion limit is hit, that results in a compile-time error. In general, it’s better not to use these types at all than to write something that fails on more realistic examples.
See more at the implementation. "
---
" Just as a refresher, a mapped type can create new object types based on arbitrary keys
type Options = { [K in "noImplicitAny"
| "strictNullChecks" | "strictFunctionTypes"]?: boolean |
or new object types based on other object types.
/ 'Partial<T>' is the same as 'T', but with each property marked optional. type Partial<T> = { [K in keyof T]?: T[K] }; "
---
" Checked Indexed Accesses (--noUncheckedIndexedAccess)
TypeScript? has a feature called index signatures. These signatures are a way to signal to the type system that users can access arbitrarily-named properties.
interface Options { path: string; permissions: number;
// Extra properties are caught by this index signature.
[propName: string]: string | number;}function checkOptions(opts: Options) { opts.path string opts.permissions number
// These are all allowed too!
// They have the type 'string | number'.
opts.yadda.toString();
opts["foo bar baz"].toString();
opts[Math.random()].toString();}In the above example, Options has an index signature that says any accessed property that’s not already listed should have the type string
| number. This is often convenient for optimistic code that assumes you know what you’re doing, but the truth is that most values in JavaScript? do not support every potential property name. Most types will not, for example, have a value for a property key created by Math.random() like in the previous example. For many users, this behavior was undesirable, and felt like it wasn’t leveraging the full strict-checking of --strictNullChecks. |
That’s why TypeScript? 4.1 ships with a new flag called --noUncheckedIndexedAccess. Under this new mode, every property access (like foo.bar) or indexed access (like foo["bar"]) is considered potentially undefined. That means that in our last example, opts.yadda will have the type string
| number | undefined as opposed to just string | number. If you need to access that property, you’ll either have to check for its existence first or use a non-null assertion operator (the postfix ! character). |
---
"
RBS
RBS is a language to describe the types of Ruby programs.
Type checkers including TypeProf? and other tools supporting RBS will understand Ruby programs much better with RBS definitions.
You can write down the definition of classes and modules: methods defined in the class, instance variables and their types, and inheritance/mix-in relations.
The goal of RBS is to support commonly seen patterns in Ruby programs and it allows writing advanced types including union types, method overloading, and generics. It also supports duck typing with interface types.
Ruby 3.0 ships with rbs gem, which allows parsing and processing type definitions written in RBS. The following is a small example of RBS with class, module, and constant definitions.
module ChatApp? VERSION: String class Channel attr_reader name: String attr_reader messages: Array[Message] attr_reader users: Array[User
| Bot] # ` | ` means union types, `User` or `Bot`. |
def initialize: (String) -> void
def post: (String, from: User | Bot) -> Message # Method overloading is supported.
| (File, from: User | Bot) -> Message
endendSee README of rbs gem for more detail. TypeProf?
TypeProf? is a type analysis tool bundled in the Ruby package.
Currently, TypeProf? serves as a kind of type inference.
It reads plain (non-type-annotated) Ruby code, analyzes what methods are defined and how they are used, and generates a prototype of type signature in RBS format.
Here is a simple demo of TypeProf?.
An example input:
An example output:
$ typeprof test.rb
You can run TypeProf? by saving the input as “test.rb” and invoke a command called “typeprof test.rb”.
You can also try TypeProf? online. (It runs TypeProf? on the server side, so sorry if it is out!)
See the documentation and demos for details.
TypeProf? is experimental and not so mature yet; only a subset of the Ruby language is supported, and the detection of type errors is limited. But it is still growing rapidly to improve the coverage of language features, the analysis performance, and usability. Any feedback is very welcome. " -- [9]
---
https://startup-cto.net/10-bad-typescript-habits-to-break-this-year/
---
brundolf 12 days ago [–]
From a quick glance this looks like a further subsetting a la strict mode, which isn't really what I meant
I clarified in another thread, but what I meant to convey is a way of giving very specific hints about specific pieces of one codebase:
"Function X will only ever take two arguments, they will be of types Y and Z"
"This object will only ever have these properties; it will never have properties created or deleted"
"This prototype will never be modified at runtime"
This could guarantee ahead-of-time that certain optimizations - packing an object as a struct instead of a hashmap, for example - can be done, so that V8 doesn't have to spend time speculating about whether or not to JIT something
reply
bastawhiz 11 days ago [–]
The problem is less about the annotations (you can already infer most of this from a single pass over the code) than it is about the calls. If you have a reference to a function, you need that data handy. Unless you're copying it around with your function reference, you don't have that data (and it's prohibitively expensive to try).
JS is heavy on function references (closures are one of the most popular JS idioms), so it's not easy to know at call time how you can optimize your code.
reply
chmod775 11 days ago [–]
>"This object will only ever have these properties; it will never have properties created or deleted"
>"This prototype will never be modified at runtime"
You can already give these hints with Object.freeze/Object.seal
Not really hints though, they enforce a certain behavior. Because hints aren't enough. A JS engine may already assume you'll never change the objects, but it still has to support cases where you then do so anyways.
I don't think these alone would enable any substantial speedups, since the performance issues arise where unknown objects are used.
reply
---
https://cglab.ca/~abeinges/blah/everyone-poops/#leakpocalypse
---
newpavlov 1 day ago [–]
Yes, a number of people have suggested introduction of a general do notation (or its analog) instead of usecase-specific async/awayt syntax, but since Rust does not have proper higher kinded types (and some Rust developers say it never will), such proposals have been deemed impractical.
reply
pdpi 1 day ago [–]
It’s not just HKTs. Figuring out how to handle Fn, FnOnce?, FnMut? is a whole other can of worms.
reply
smt1 1 day ago [–]
I think there were some (related, I think!) proposals here: https://github.com/rust-lang/lang-team/issues/23 https://github.com/rust-lang/rfcs/issues/3000
reply
---
withoutboats on July 16, 2018 [–]
Here are three problems:
Higher kinded polymorphism results in trivially undecidable type inferences without something like currying; the restrictions needed to support it would be arbitrary and weird given that Rust does not have currying (essentially some rules to reconstruct the restrictions of currying in type operator context).
Instances of both Future and Iterator do not implement the Monad type class as defined in Haskell, because the "fmap" operator does not return the "self" type parameterized by a new type, it returns it own new type. This is because the state machine they represent is leaked through their function signature.
Do notation doesn't work with the imperative control flow that Rust has, which other people have already discussed.
---
i guess what's fundamentally needed for Oot to have a programmable type system that can accomodate something like Rust is first-class analysis of relationships between variables and values (e.g. only one variable can own a value at a time; variables can borrow references; there can be only one borrow in a scope if there are any mutable borrows in that scope; etc).
---
" We use the Schema library for defining datatypes within our codebase. It’s easy to use and we like the flexibility to define schema constraints beyond just types: e.g. arbitrary predicates, enums, and unions. Our codebase contains about 600 type definitions, most of which are annotated using Schema.
Around Schema we have a helper called "defrecord+" which defines constructor functions which also perform validation (e.g. for type Foo it generates "->valid-Foo" and "map->valid-Foo"). These functions throw a descriptive exception if the schema check fails. " [10]
---
"Python's type annotation syntax is shoe-horned to minimize changes to the parser--if you're allowing yourself to rewrite the parser, why not improve the type annotations? Indeed, why not stick to a more Rust-like syntax in general?)." [11]
---
re: monads
mrspeaker 5 days ago [–]
If you never want to learn Haskell (or PureScript? or similar) then the author even says in the `If They're So Wonderful Why Aren't They In My Favorite Language?` section:
"If you don't need IO sequencing, or purity because your language doesn't care about purity, or the list implementation's nondeterminism because that's a parlor trick, or STM because your ecosystem doesn't use it... there's not much point to worrying about it. Monad implementations in languages other than Haskell fail to take off because there generally isn't even a single thing that is improved by working with it through a monad interface, let alone a family of such things."
"[...]It's definitely an interesting idea, and if you are a curious programmer, it's worth learning about this particular interface and what it can do. But it's not something you generally directly take back to your language"
---
avalys 5 days ago [–]
I feel like these tutorials always fall apart when they start introducing Haskell syntax and say "That's Monad, simple as that!"
class Functor f where
flip fmap :: f a -> (a -> b) -> f b
class Monad m where
(>>=) :: m a -> (a -> m b) -> m bSorry, that's not doing much for me! I am now going to look for a tutorial on Monads that's written in, say, Python, so at least I don't have to learn an abstract new language alongside the abstract new concept.
reply
wyager 5 days ago [–]
> I am now going to look for a tutorial on Monads that's written in, say, Python
It probably won’t be very helpful. The definition of a monad is 90% in the types.
People use Haskell to talk about monads for two reasons:
1. Its type system is expressive enough to represent them (parametric polymorphism and higher-kinded types)
2. It’s one of a very small number of languages that doesn’t let users wiggle their way around needing some kind of principled effect system, so you really can’t get away without monads. Only in such an environment can the social pressure to take shortcuts be overcome, forcing people to structure their code carefully enough that the rich concept of monads isn’t reduced to a few occasionally used and probably incorrectly implemented corner cases like optional values and maybe futures.
reply
---
eqvinox on April 14, 2020 [–]
What's the best way to deal with "transitive const-ness", i.e. utility functions that operate on pointers and where the return type should technically get const from the argument?
(strchr is the most obvious, but in general most search/lookup type functions are like this...)
Add to clarify: the current prototype for strchr is
char *strchr(const char *s, int c);
Which just drops the "const", so you might end up writing to read-only memory without any warning. Ideally there'd be something like:
maybe_const_out char *strchr(maybe_const_in char *s, int c);
So the return value gets const from the input argument. Maybe this can be done with _Generic? That kinda seems like the "cannonball at sparrows" approach though :/ (Also you'd need to change the official strchr() definition...)
pascal_cuoq on April 14, 2020 [–]
Speaking as someone who is not in the committee but has observed trends since 2003 or so, I would say that solving this problem is way beyond the scope of evolutions that will make it in C2a or even the next one.
There are plenty of programing languages that distinguish strongly between mutable and immutable references, and that have the parametric polymorphism to let functions that can use both kinds return the same thing you passed to them, though. C will simply just never be one of them.
DougGwyn? on April 14, 2020 [–]
Many uses of strchr do write via a pointer derived from a non-const declaration. When we introduced const qualifier it was noted that they were actually declaring read-only access, not unchangeability. The alternative was tried experimentally and the consequent "const poisoning" got in the way.
coliveira on April 14, 2020 [–]
I believe C is doing the right thing. Const as immutability is a kludge to force the language to operate at the level of data structure/API design, something that it cannot do properly.
---
state machines in Rust. I think this is an example of 'type level programming' (the compiler is checking that the state is Green at the time that you make the allow_bikes(&state) function call) so i'm probably not down for it in oot: https://blog.yoshuawuyts.com/state-machines/
this comment talks about the analogous think in C++20: https://news.ycombinator.com/item?id=22747184
they talk about the P language:
Phlogistique on April 1, 2020 [–]
They link to the `P` language, which I did not know about.
I found the link interesting because I have at times wondered what it would look likes if FSM were first class control flow features, akin to `if` and `while`.
wiz21c on April 1, 2020 [–]
the ping pong program is very easy to read. I don't know if it scales to bigger ones, but this one is really nice.
palotasb on April 1, 2020 [–]
https://github.com/p-org/P/wiki/PingPong-program for anyone else wondering
---
Statecharts sound cool
some discussion: https://news.ycombinator.com/item?id=22746708
---
this guy says state machines can often be replaced by generators:
https://news.ycombinator.com/item?id=22750734
---
---
https://blog.pentlander.com/building-blocks-sasquach-type-system/ https://lobste.rs/s/oj8lul/building_blocks_sasquach_type_system
---
masklinn on July 27, 2012 [–]
The haskell code is — as far as I can see anyway — nominative typing. It can be post-implemented, but you still need your type to be explicitly made into a Stream instance.
Contrast OCaml, an object type is represented as a set of (method, types) tuples and type-checking is a subset check (if type A has all the methods of type B, then it's a subtype of B regardless of anything else from visibility to semantics):
---
eru on July 27, 2012
| parent | favorite | on: Go is boring |
Static typing also makes overloading your f.unctions on return type instead of just arguments types possible. Not a lot of languages do this, though. I only know of one, but it's invaluable there.
---
---
my comment:
https://lobste.rs/s/oa8sgi/four_noisy_horsemen_perl_hate#c_i4oo7u
bshanks edited less than a minute ago
| link | edit | delete | flag |
I think one thing that makes Perl hard to read is Perl’s idea of list/scalar context, which I believe is a form of ad-hoc polymorphism. jbert posted this link introducing scalar/list/void context in Perl: https://www.perlmonks.org/?node_id=738558
The article makes it sound like sigils are just clarifying what type things are, and wouldn’t that improve readability? But because of context, sigils in Perl aren’t just like type annotations that help clarify and double-check what’s already going on, rather they are actually choosing which of the overloaded meanings of the annotated expression is being run.
Some other programming languages have ad-hoc polymorphism based on how the value of an expression is later used, as well. In my opinion this can be powerful but can make things less readable; you can no longer understand code by “single-stepping” with your eyes from the first thing computed to the last.
---
mikebike on July 27, 2012
| unvote | parent | favorite | on: Go is boring |
Perl's a dynamic language, but return type can vary based on context. I once saw this really bite someone where the presence of parentheses on the left-hand side of the expression changed the behavior of the function being called on the right-hand side. Not fun to debug that one.
---
https://lobste.rs/s/otrxxf/problem_effects_rust_2020
5 yossarian 7 days ago
| link |
This is a well-written post, but I think I disagree with the author w.r.t. this actually being a problem: effects within closures and iterators are subtle things, and I prefer Rust’s approach of requiring users to explicitly ferry them into the surrounding context.
It also tends to be only a minor hiccup in practice: collect can be used to flatten a sequence of Result<T>s into Result<Container<T>>, which is the intuitive and intended behavior in almost all circumstances.
1
cyberia 7 days ago | link | Oh cool, I didn’t know about this. Can it do the same with an iterator of Future<T>s into a Future<Container<T>>?
Actually thinking about it, I guess not, because there’s a choice to be made about whether to do them all in parallel or in sequence.
3 cyberia edited 8 days ago
| link |
I really like this article. Learning Rust from a Haskell background, I’ve been coming across the annoyance of not being able to use ? inside a closure, and thinking about it as a consequence of Rust not having monads. I hadn’t thought about the TCP-preserving-function style at all.
I tend to agree with the author though that it seems unlikely that Rust will address this problem any time soon. And to be honest, I’m alright with that. I think given that Rust only has the three effects mentioned (or four if you count memory ownership as an effect), it’s an at worst “OK” solution to simply combine them ad-hoc (like Iterator::map_while or tokio::StreamExt::map etc.). It works OK-ish for TypeScript?.
2 tathanhdinh edited 8 days ago
| link |
It’s not clear for me what the author means when saying:
Rust’s design philosophy has landed on the principle that all effect points should be marked in the program source, including forwarding, so that users can more easily reason about the control flow of their program.
That may be true for exceptions (which Rust abandon completely), but there are more (e.g. divergence, heap allocation, etc.) kinds of effect which have nothing with control flow.
Rust has an excellent system for managing effects related to mutation and memory: this is what ownership and borrowing is all about, and it beautifully guarantees soundness even in the presence of concurrent mutation.
IMHO, this is not true, Rust does not manage effects for mutation and memory, it rather forbids that with ownership and borrowing. Consequently, its type system is limited, e.g. (co-)recursive types cannot be represented naturally in Rust.
4
alilleybrinker 7 days ago | link | Genuinely curious, what do you consider unnatural about recursive types in Rust? Rust’s lack of implicit boxing means you need to wrap the recursion in Box, but that’s what happens under the hood in other languages anyway. Perhaps there are forms of recursive types which you’re thinking of, but I’m uncertain what they’d be.
1
tathanhdinh edited 6 days ago | link | I’m not sure that other languages use box (or reference, etc) to implement recursive types at low-level, but that’s irrelevant since we are talking about the expressiveness of the type system. For example, one way to represent a list type in Rust is:
enum List<T> { Cons(T, Box<List<T>>), Nil }First, this type is not a representation for the functional definition of a list (i.e. Fix(\L.Nil + Cons(T, L)). Second, since an argument about a infinite size of such a type, at a “high enough” level as type system, why we need to care whether a type is located on heap (since box) or not: the type checking should proceed before deciding where some variable of this type is stored.
Come back to the article, I’m quite confused about “effect”, e.g.
Falliblity: The effect of a section of code failing to complete and evaluate to its expected value (in Rust, think Result)
Result is not effect, it’s a type, as the language has no support to reason about “a section of code failing to complete”. Using Result just helps forcing the programmer to rest in the Ok(s) railway, but this has nothing about effect.
The article said about using monad, as in Haskell. but note that Haskell does that because it is essentially has no support for effect (then it has to “simulate” effect by the type system). We may note that effect checking is not the same as type checking, e.g. suppose a function f : () -> <E> T where <E> is the notation for an effect E, and g : T -> <E'> T' then g ° f should type check (by a language supporting effect) since it’s not always g which has to handle the effect E.
---
sqlite 'STRICT' mode:
" The datatype must be one of following:
INT
INTEGER
REAL
TEXT
BLOB
ANY
"[14]---
https://google.github.io/pytype/typing_faq.html
---
" Why is Optional[Optional[T]] the same as Optional[T]?
Consider the following code:
x: Dict[str, Optional[str]] = {'a': 'hello', 'b': None} a = x.get('a') b = x.get('b') c = x.get('c')
Since the signature of dict.get is
class Mapping(Generic[K, V]): def get(key: K) -> Optional[V]
an ML-based language would indeed have a return type of Optional[Optional[str]], and be able to distinguish a value of None from a missing value. This comes down to the fact that python has union rather than sum types; Optional[T] is an alias for Union[T, None], and therefore, by a series of expansions,
Optional[Optional[T]]
Note that this is simply a difference of behaviour, not a flaw in either python or pytype; in particular Optional being a sum type would mean Optional[T] was an alias for None
| Some[T] rather than None | T, which would mean every dictionary key access would need to be unwrapped before being used. |
--
"
You can have type level programming without distinguishing between type level programming and value level programming. Dependent types achieves this, by making types and values live in the same namespace. " [15]
---
" related threads:
https://news.ycombinator.com/item?id=26378141 and https://lobste.rs/s/lng3c0/announcing_rust_1_50_0 (Rust following C++)
https://lobste.rs/s/9rrxbh/on_types#c_qanywm and https://news.ycombinator.com/item?id=26378696 (Type checking vs. metaprogramming)
https://news.ycombinator.com/item?id=27026990 (debugging and profiling macros, Andy Kelley chimes in on the “1000 backward branches” rule in Zig)
https://news.ycombinator.com/item?id=21310029 (MyPy? inhibits metaprogramming; it’s basically a different language than Python. I use it in Oil for predictable speed via translation to C++, not really for correctness)
" -- https://lobste.rs/s/pkmzlu/fsharp_designer_on_downsides_type_level#c_hhcmho
---
~
zenhack 13 hours ago | link | flag | Fwiw, even in Haskell you only really need one extension to obviate type classes in terms of “expressiveness,” namely RankNTypes?. See https://www.haskellforall.com/2012/05/scrap-your-type-classes.html…though it doesn’t solve the verbosity issues. But I suspect that a language with better support for records might make this a pretty good solution (I have a side project where I am working on such a language).
~
singpolyma 9 hours ago | link | flag | RankNTypes? is my top pick for something to add to Haskell. however, for common cases type classes have the advantage of having decidable inference.
-- https://lobste.rs/s/pkmzlu/fsharp_designer_on_downsides_type_level#c_jkbyqb
---
disadvantages of type classes:
https://github.com/fsharp/fslang-suggestions/issues/243#issuecomment-916079347
---
7 janus 3 days ago
| link | flag |
You can have type level programming without distinguishing between type level programming and value level programming. Dependent types achieves this, by making types and values live in the same namespace.
1
kevinc 2 days ago (unread) | link | flag | Do you have any favorite examples?
6
janus edited 2 days ago (unread) | link | flag | Dependent types make stuff like type families, GADTs and kinds obsolete, which are all special-cased in Haskell today.
So since we’re talking about removing code, I it is weird to bring an example. But really just take any arbitrary type family, and that can serve as an example.
A function like this has to be written using a type family or GADT in Haskell:
the (Bool -> Type) (\x => if x then Float else Int)
(this is Idris syntax)
2
owl 2 days ago (unread) | link | flag | Does that mean Zig has some form of dependent types?
fn the(x: bool) type { return if (x) f64 else i64; }
pub fn main() void { @import("std").debug.warn("wee " ++ @typeName(the(true))); }
4
smaddox edited 2 days ago (unread) | link | flag | I would say that Zig does have dependent types, but it’s dependent type system is “unsound”, in the sense that a function call can type check in one use case but might fail type checking in another use case, due to how types are only checked after use and monomorphization. It’s arguably better than not having them at all, though, and I think that’s born out in practice.
It certainly limits the value of dependent types, though. You can’t reliably use Zig’s type system as a proof assistant in the way that you can use Coq’s, Agda’s, or Idris’s.
---
11 smaddox 13 hours ago
| link | flag |
Very insightful. I do find type level programming in Haskell (and, to a lesser extent, Rust) to be a confusing nightmare. Nonetheless, Rust could not exist without traits (i.e. without bounded polymorphism). The Sync and Send marker traits (combined with borrow checking) are the basis of thread safety.
I think Zig takes an interesting approach here, with it’s compile-time programming (i.e. type level programming with the same syntax and semantics as normal programming), but it suffers from the same typing issues as C++ templates, i.e. types are only checked after use and monomorphization. Rust’s bounded polymorphism can and is type checked before monomorphization, so you know if there are type errors in general. In Zig (and C++), you only know if there are type errors with a particular type, and only after using a function (template) on that type.
I think there’s room for an approach that’s more like Zig’s, but with sound polymorphic typing, using dependent type theory. Coq, Agda, and Idris include type classes (aka implicits, bounded polymorphism), but it doesn’t seem like type classes should be necessary in a dependently typed language. In particular, it doesn’t seem like they should provide any increase in expressiveness, though perhaps they reduce verbosity.
~
zenhack 13 hours ago | link | flag | Fwiw, even in Haskell you only really need one extension to obviate type classes in terms of “expressiveness,” namely RankNTypes?. See https://www.haskellforall.com/2012/05/scrap-your-type-classes.html
…though it doesn’t solve the verbosity issues. But I suspect that a language with better support for records might make this a pretty good solution (I have a side project where I am working on such a language).
~
singpolyma 9 hours ago | link | flag | RankNTypes? is my top pick for something to add to Haskell. however, for common cases type classes have the advantage of having decidable inference.
~ enobayram 3 hours ago
| link | flag |
Type classes aren’t just about verbosity, global coherence is a very important aspect. Any decision on whether to use a type class vs. explicit dictionary passing needs to consider the implications of global coherence. I think Type Classes vs. the World is a must-watch in order to engage in productive discussion about type classes.
---
" For example, I think it brings me joy as a reader that I can tell at a glance from a function signature which arguments are modified and which ones are just read. Without the abstraction of mutable and immutable references I would have to read the entire source code of the function and every function it calls to know for sure what it does with the pointers. It also brings me joy as a reader that common functionality like equality comparisons or string formatting can be derived by the compiler, instead of having separate hand-made implementations for each data structure, which might have subtle differences. "
---
"For me, it is the combination of algebraic data types + pattern matching + compile time exhaustiveness checking that is the real game changer" [16]
---
Turnstile+: Dependent Type Systems as Macros
In 2017, a team from Northeastern University released Turnstile, a framework for implementing propositionally typed languages in Racket; cf. naasking's story Type Systems as Macros. The system was really nice because it allowed type systems to be expressed in a manner similar to the way theoretical PL researchers would in a paper, and because it hooked into Racket's clean compiler backend.
Now Stephen Chang, one of that team, together with new coauthors Michael Ballantyne, Usamilo Turner and William Bowman, have released a rewrite that they call Turnstile+, together with a POPL article, Dependent Type Systems as Macros. From that article's introduction:
http://www.ccs.neu.edu/home/stchang/pubs/cbtb-popl2020.pdf
https://github.com/stchang/macrotypes http://lambda-the-ultimate.org/node/5587
---
"Monads let you concentrate on functions by providing a sort of side channel for information associated with those functions. For example, you may have a drawing program and want to compose a rotation and stretching. These may be ostensibly pure functions, but they also effect a log of operations that lets you undo actions. It would be burdensome to consider this log as an explicit argument passed into and returned from every operation. so you might keep this log information in a monad." -- [17]
that seems right to me, and the example of impure undo alongside pure functions is a great example for what we need to achieve with Oot's effects system (the other example i always have in mind is logging) altho this lobste.rs commentator thinks it's too narrow:
"Maybe is a monad. It sequences computations that can fail. There is no side channel of information at all there; a computation either fails or doesn’t. Not to mention the Sum and functions (->) which are also monads and can’t be thought of as having any side channel – they compose actions. Or Product which combines functors. This is not a good mental model for monads." -- https://lobste.rs/s/6cwnlc/monads_macros#c_lvvbap
also a replier supports the original article: "It resembles my own mental model. Monads sweep repetitive logic under the rug and let you focus on a chain of computations. Methods from particular monads—not part of the Monad interface itself—let you access or interact with that submerged logic. My other mental model is “statements, but made out of expressions”"
the first commentator also mentions some uses of Haskell macros in popular libs: "some of the most popular Haskell libraries use macros like lens (Control.Lens.TH) and aeson (Data.Aeson.TH)."
---
The only thing that should need explicit typing is public function prototypes (private function prototypes can be inferred)
---
https://nora.codes/post/its-time-to-get-hyped-about-const-generics-in-rust/
---
https://manishearth.github.io/blog/2018/02/01/a-rough-proposal-for-sum-types-in-go/
---
consider https://www.w3.org/TR/owl2-profiles/#OWL_2_EL , an ontology language with polytime inference (it's a restrictive description logic) - https://www.researchgate.net/publication/305560717_Semantic_Object-Oriented_Programming_SOOP - https://arxiv.org/abs/1907.00855 Type Checking Program Code using SHACL (Extended Version) - trioo
---
https://verdagon.dev/blog/higher-raii-7drl https://lobste.rs/s/3evayg/vale_s_higher_raii_pattern_saved_me_vital_5
---
Type Systems as Macros
https://news.ycombinator.com/item?id=14167620 https://web.archive.org/web/20211228002353/https://www.ccs.neu.edu/home/stchang/popl2017/ https://web.archive.org/web/20211128175738/https://blog.racket-lang.org/2017/04/type-tailoring.html
LightMachine? on April 22, 2017
| parent | context | prev | next [–] | on: Type Systems as Macros |
eli5?
chriswarbo on April 22, 2017
| parent | next [–] |
Macros are run at compile time, and are used to rewrite source code prior to interpretation or compilation. They're mostly used to make nicer syntax, e.g. a macro could turn an expression like `(with-file (f "/tmp/foo") ...)` into a working implementation like:
(let* ((f (open "/tmp/foo"))
(result ...))
(close f)
result)Here, the authors make macros for type annotations, i.e. they take expressions like `(my-value : my-type)`, check whether the types unify correctly, and spit out an untyped expression implementing that value if they do.
By using macros, the type system becomes modular: new type system features (subtyping, kinds, etc.) can be written by the programmer as a set of macros, rather than as a whole new language (and all of the work that entails). They test their claim by implementing a bunch of features, combining/reusing them in a bunch of mini languages, and write some semi-plausible programs in these languages, to see if they're realistic.
stchang on April 26, 2017
| parent | next [–] |
This approach works well because the surface and core languages are similar, and thus the type checker need only handle a small number of core forms.
This approach is limited, however, to constructs that are translatable into the core typed language. For example, a few Racket `for/X` comprehension forms are not supported in Typed Racket because they are difficult to translate.
Our approach alternatively uses macro expansion to type check the surface language and translates it into an untyped core language. Thus it's less limited in the typed languages one may implement. The tradeoff is that the programmer must implement type rules for all forms in the surface language, rather than just the core language.
juliangamble on April 23, 2017
| prev | next [–] |
How powerful is the type system? Can you do dependent types?
stchang on April 26, 2017
| parent | next [–] |
> Can you do dependent types?
Yes. For example, see https://github.com/wilbowma/cur
https://web.archive.org/web/20211009023726/lambda-the-ultimate.org/node/5426
Type Systems as Macros
Type Systems as Macros, by Stephen Chang, Alex Knauth, Ben Greenman:
We present TURNSTILE, a metalanguage for creating typed embedded languages. To implement the type system, programmers write type checking rules resembling traditional judgment syntax. To implement the semantics, they incorporate elaborations into these rules. TURNSTILE critically depends on the idea of linguistic reuse. It exploits a macro system in a novel way to simultaneously type check and rewrite a surface program into a target language. Reusing a macro system also yields modular implementations whose rules may be mixed and matched to create other languages. Combined with typical compiler and runtime reuse, TURNSTILE produces performant typed embedded languages with little effort.
This looks pretty awesome considering it's not limited to simple typed languages, but extends all the way to System F and F-omega! Even better, they can reuse previous type systems to define new ones, thereby reducing the effort to implement more expressive type systems. All code and further details available here, and here's a blog post where Ben Greenman further discusses the related "type tailoring", and of course, these are both directly related to Active Libraries.
Taken to its extreme, why not have an assembler with a powerful macro system of this sort as your host language, and every high-level language would be built on this. I'm not sure if this approach would extend that far, but it's an interesting idea. You'd need a cpp-like highly portable macro tool, and porting to a new platform consists of writing architecture-specific macros for some core language, like System F.
This work may also conceptually dovetail with another thread discussing fexprs and compilation.
Home Type Systems as Macros
Type Systems as Macros, by Stephen Chang, Alex Knauth, Ben Greenman:
We present TURNSTILE, a metalanguage for creating typed embedded languages. To implement the type system, programmers write type checking rules resembling traditional judgment syntax. To implement the semantics, they incorporate elaborations into these rules. TURNSTILE critically depends on the idea of linguistic reuse. It exploits a macro system in a novel way to simultaneously type check and rewrite a surface program into a target language. Reusing a macro system also yields modular implementations whose rules may be mixed and matched to create other languages. Combined with typical compiler and runtime reuse, TURNSTILE produces performant typed embedded languages with little effort.
This looks pretty awesome considering it's not limited to simple typed languages, but extends all the way to System F and F-omega! Even better, they can reuse previous type systems to define new ones, thereby reducing the effort to implement more expressive type systems. All code and further details available here, and here's a blog post where Ben Greenman further discusses the related "type tailoring", and of course, these are both directly related to Active Libraries.
Taken to its extreme, why not have an assembler with a powerful macro system of this sort as your host language, and every high-level language would be built on this. I'm not sure if this approach would extend that far, but it's an interesting idea. You'd need a cpp-like highly portable macro tool, and porting to a new platform consists of writing architecture-specific macros for some core language, like System F.
This work may also conceptually dovetail with another thread discussing fexprs and compilation. By naasking at 2017-04-19 23:38
| DSL | Functional | Lambda Calculus | Meta-Programming | Type Theory | other blogs | 52900 reads |
comparison with Shen
Hi, Thanks for your interest.
Our paper presents a method for implementing typed DSLs, particularly type checkers for these DSLs, using only an off-the-shelf macro system, namely Racket's.
Our method is pragmatic since it is compatible with the way Racket programmers already implement (untyped) DSLs, as a series of macro definitions. We show that these DSL creators may add type checking to their language simply by extending their macro definitions with a protocol for communicating the necessary type information. As a result, type checking is computed as part of macro expansion, hence "type systems as macros". Finally, we add a syntactic layer (Turnstile) that enables defining these type-checking macros using a declarative syntax that roughly resembles conventional type rule specifications.
In contrast, Shen appears to already come with a full-featured type system out of the box. Programmers then extend this type system via a special-purpose framework that allows defining new datatypes in a sequent-calculus-style syntax. Thus Shen seems to fall under the "extensible type systems" line of work?
Implementing typed DSLs with extensible type systems is typically more restrictive than our approach because the base type system constrains both the features that *may* be added and the features that *must* be included in any DSL. Shen's extension framework seems sufficiently expressive such that the former may not be much of problem, but I think the latter still might be an issue? In other words, can a DSL writer take away unwanted type system features? For example, can one reuse Shen's type system to create a simply-typed DSL where polymorphism is not allowed? How about defining a new function application rule for a DSL with a type-and-effect system? Or how about a DSL with completely different base types, e.g., Int for integers instead of Number?
Implementationwise, neither Shen's base type system nor its extension rules appear to desugar into plain macro definitions. Instead, I think they correspond to rules in an underlying logic language? In short, I do not see "type systems as macros" in any of the linked examples and thus I do not understand the similarity assertions. Would "type extensions as logic programs" be a more accurate description of Shen? By stchang at Thu, 2017-05-18 19:39
| login or register to post comments |
---
this article ends up thinking that Idris solves the problem of duplication/different syntax between type-level and value-level but is too complex, and that Zig's comptime is the best actual answer so far:
https://hirrolot.github.io/posts/why-static-languages-suffer-from-complexity.html
---
i've seen two ppl recommend this as the current best way to typecheck:
Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism
---
---
"you will also notice (if you compare) where unconventional implementation choice is made for simplicity. For example, poly’s type inference is done without unification because it is simpler to do everything with substitution, but real implementations don’t do that due to efficiency reasons." -- [18]
---
adaszko edited 1 hour ago
| link | flag |
but there’s also a deep anxiety that one day I’ll come across a feature or qwerk that I just can’t wrap my head around and it blocks my progress indefinitely.
I share the sentiment of feeling blocked indefinitely sometimes. Rust’s type checking (and not only Rust’s) lacks incrementalism in the sense that with when you get a runtime error, you have all sorts of tools to help you narrow down the issue: print(), debuggers, deleting parts of the program and seeing if the issue persists, etc. With type checking OTOH, you just get the nice, terse No ;) with some not always helpful error message. One way to address this issue would be of course to make the compiler explain its reasoning step-by-step so that you can see where your reasoning diverges from the compiler’s but that’s a tall order. If it comes to lifetimes, I think there should be a way to dump the code with all the lifetimes inferred by the compiler so that we can compare them with our expectations (that would have been really helpful for me at the learning stage, back when I hadn’t memorized all the lifetime elision rules). Another way to make debugging type checking errors easier would be to get more incrementalism by way of making it possible to break down any code into a series of easy-to-comprehend partial expressions of the form let var_introduced_purely_for_comprehension_purposes: ComprehensibleType? = short_expression that later combine into the final, desired expression that’s trivially of the right type. The reason we can’t always do that today is that some types are so big that are better left untold, like a combination of iterators (impl Trait types do not always work or they don’t constraint the type enough).
Another major complicating factor is the return type polymorphism (along with the turbofish). Ideally, method dispatch would only work one way but it’s obviously too late for that (that’s something Zig has as a design goal BTW). The next best thing I think is to add support for debugging it in the IDE: something like a “get the type of the selected expression” functionality in rust_analyzer. Type ascriptions could help too as they’re more flexible than turbofish.
-- [19]
---
matklad 3 hours ago
| link | flag |
Rust is three-five languages in a trench coat:
imperative plain rust code: for x in [1, 2, 3] (with a subset for const)
substitution-based macros: macro_rules! { /*this looks nothing like Rust*/} + proc-macros
logical traits (impl X for Y where Z:T)Zig is very uniformly just one imperative language.
This I think is the major reason why Zig feels smaller.
~
jado 1 hour ago | link | flag | Very true! I recently rewrote a packet struct generator I made a few years ago in Rust to Zig. The original implementation used heavy Rust macros to manipulate types, while the Zig implementation doesn’t require anything special because I can manipulate types as values. The comptime reflection is crazy cool, and felt more intuitive to me than building this pseudo-DSL for packet definitions.
-- [20]
---
" Actually, with ML modules, orphan rules go away because choosing implementations of your trait-ish things is explicit. The classic example of trait conflicts that I like is you have module A that provides type A.T and implements Hash on it, then you have module B that implements its own copy of the Hash trait on type A.T with a different hashing algorithm. Now whenever you get an A.T and pass it to something you don’t know whether it should use A’s implementation of Hash or B’s implementation of Hash
This doesn’t happen with modules ‘cause it extracts the implementation from the type. Rust-style traits basically have a list of implementations of traits attached to each type, which is global. ML modules have a list of implementations of traits that are not attached to particular types, they live in your module namespace like any other value, so if your function is passed an A.T and wants to hash it then it also has to know what implementation its using. If something creates an Hashset<A.T, A.Hash> or whatever and passes it to a function that is using B.Hash then it won’t typecheck.
The downside of this is that juggling this by hand instead of using the type as your namespace is kinda a pain in the ass. " -- [21]
---
" It is no coincidence that modern JavaScript? programming with TypeScript? has some congruency with C# given that Anders Hejlsberg was the lead architect of the C# language and also led development of TypeScript?.
https://miro.medium.com/max/1320/0*t_WTNE8tIBevZ973 " -- [22]
---
https://ucsd-progsys.github.io/liquidhaskell-blog/
---
https://smallcultfollowing.com/babysteps/blog/2022/09/22/rust-2024-the-year-of-everywhere/#fn:moro
--- " For instance, I commonly see new Rust developers doing something like this:
fn double_or_multiply(x: i32, y: Option<i32>, double: bool) -> Result<i32> { if double { if y.is_some() { return Err("Y should not be set"); } x * 2 } else { if y.is_none() { return Err("Y should be set"); } x * y.unwrap() } }
Yes, I know its a completely contrived example, but I’m sure you’re familiar with that kind of pattern in code. The issue is that this is using the shallow aspects of Rust’s type system – you end up paying for all of Rust but only reaping the benefits of 10% of it. Compare that to what you could do by leveraging the type system fully:
enum OpKind? { Double(x), Multiply(x, y), }
fn double_or_multiply(input: OpKind?) -> i32 { match input { Double(x) => x * 2, Multiply(x, y) => x * y, } }
"
-- [23]
---
https://twitter.com/iavins/status/1524407933982765056
"I recently discovered pytype, a static type analyser for Python from Google that figures out types from the static analysis. In contrast, mypy relies on annotations.
Following code passes mypy, but pytype recognises that `str.join` requires an iterable, not individual strings!"
---
~
andyc 6 hours ago | link | flag | Related
Mojo doesn’t support overloading solely on result type, and doesn’t use result type or contextual type information for type inference, keeping things simple, fast, and predictable. Mojo will never produce an “expression too complex” error, because its type-checker is simple and fast by definition.
https://docs.modular.com/mojo/notebooks/HelloMojo.html#overloaded-functions-methods
---
i think i like these decisions:
[25] ---
antigoal: "Anything requiring a proof solver as part of the type system" -- [26]
---
https://github.com/metosin/malli
---
---
" AviKav? 35 hours ago
| link | flag |
Viewpoint adaptation?
~
david_chisnall 25 hours ago (unread) | link | flag | The idea that the type of a value depends on the types of pointers that you followed to get to it. If you have an immutable pointer to an object, all of its fields are immutable. This lets us express region semantics because the region associated with an object flows through the type system from the pointer that you followed into that region. "
---
