Just foxing about.
Comment by ~icefox on ~icefox/garnet
Resolved in commit 339:2875b8b9760b https://hg.sr.ht/~icefox/garnet/rev/2875b8b9760bd4554e6c0d821359119b2d8139b1
Comment by ~icefox on ~icefox/garnet
There's two parts to this currently, which are kinda hilariously opposite:
- The parser produces nice-ish error messages with codespan, but only ever panics on error, not returns
Results.- The rest of the compiler has pretty nice
Result's with a fair amount of work put into making them informative, but the HIR contains no span info.So we need to do both: Parser needs to give
Result's, and the HIR needs to contain span info for something resembling the expression it corresponds to.
Comment by ~icefox on ~icefox/garnet
A proof-of-concept-ish idea for properties may be to simply allow users to annotate arbitrary properties onto things, and make them "sticky" so that if a function/type has a property, any functions/types that use it will have the same property unless explicitly removed a la Rust's
impl !Sync for .... That may or may not be actually useful or at all like what we want in the long run, but may be enough to start playing with ideas and see if it feels good at all.
Comment by ~icefox on ~icefox/garnet
Related: https://github.com/fsharp/fslang-suggestions/issues/243
How does F# handle this sort of thing, anyway?
Ticket created by ~icefox on ~icefox/garnet
Bidirectional type checking:
- https://research.cs.queensu.ca/home/jana/papers/bidir/Dunfield13_bidir.pdf
- https://www.youtube.com/watch?v=utyBNDj7s2w
- https://www.cs.cmu.edu/~fp/courses/15312-f04/handouts/15-bidirectional.pdf
- https://ncatlab.org/nlab/show/bidirectional+typechecking
- https://www.youtube.com/watch?v=utyBNDj7s2w
System F stuff:
- https://blog.jez.io/system-f-param/
- https://www.pure.ed.ac.uk/ws/files/129967822/System_F_in_Agda_CHAPMAN_DOA14062019_AFV.pdf
- https://github.com/input-output-hk/plutus/tree/master/papers/system-f-in-agda
Conversation on HM:
superstar64 — 05/09/2021 are you familiar with impredicative instantiation? if not would you like me to explain it to you? icefox — 05/09/2021 No, and yes! If you have time someday. superstar64 — 05/09/2021 it's actually not that complicated, lets say you have a polymorphic function id :: forall a. a -> a id x = x impedance instantiation is just substituting for another polymorphic type id @ (forall a. a -> a) :: (forall a. a -> a) -> (forall a. a -> a) id @ (forall a. a -> a) apparently doing this in 1ML messes up the type inference, you need wrap to tell typecheck that your trying to do this what i don't understand is why you need this for a linked list icefox — 05/09/2021 So what is id @? superstar64 — 05/09/2021 that's type application, it substitutes a variable with a forall type, id @ Int has type Int -> Int mainstream languages call it f<T> icefox — 05/09/2021 Aha impedance instantiation is telling it what to do with id id, or calling id on any other polymorphic type? superstar64 — 05/09/2021 yes icefox — 05/09/2021 oh! Well then. superstar64 — 05/09/2021 Λa. id <a -> a> (id <a>) -- what haskell, and i imagine 1ML do by default id<forall a. a -> a> (id) impredicative version icefox — 05/09/2021 I have to wonder now why that is even a thing superstar64 — 05/09/2021 it's consistency, forall means all types, even polymorphic ones umm, it's impredicative not impedence, i always get the two mixed up icefox — 05/09/2021 Aha, I see. Thanks a lot! superstar64 — Today at 2:18 PM If you want, I can give you a quick rundown of hindley milner. (Or at least a subset of it without let generalization) icefox — Today at 2:23 PM sure! What's "let generalization"? superstar64 — Today at 2:27 PM Let generalization is the tricky part of hindley milner, where you allow things like let f = \x -> x in (f 1, f True) to work. The issue is that you almost always want let generalization at a global level and hindley milner allows it a local level. Anyway, hindley milner is an algorithm that uses unification theory for type checking. https://en.wikipedia.org/wiki/Unification_(computer_science) Unification (computer science) In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions. Depending on which expressions (also called terms) are allowed to occur in an equation set (also called unification problem), and which expressions are considered equal, several frameworks of unification are distinguished. If h... For a given term that you want type check. You generate a list of type equations and then solve them. Imagine you had something like \x -> x + 1. Here you generate a type variable for x, x :: a, and then you generate an equation, a = Int. Then later you solve your equations which gives you a substition that you can plug back into the original type. a -> Int Here, try solving this system for example a = Int b = [a] c = b In general, you want your code to look something like this: type Equations = (Type, Type, PositionData) type Substition = Map TypeVariable Type solve :: Equations -> Substition The algorithm to solve these types of equations are again on wikipedia, https://en.wikipedia.org/wiki/Unification_(computer_science)#Syntactic_unification_of_first-order_terms Where the variables are type variables, and the functions are type constructors (Array, Int, etc). Unification (computer science) In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions. Depending on which expressions (also called terms) are allowed to occur in an equation set (also called unification problem), and which expressions are considered equal, several frameworks of unification are distinguished. If h... icefox — Today at 2:41 PM yeah from what I've seen you basically have a "collect information" step and a "apply information" step sorry, a little distracted offline superstar64 — Today at 2:44 PM A lot of the hindley milner tutorials mix these steps though. icefox — Today at 2:45 PM aha superstar64 — Today at 2:45 PM The collect information and apply information gets a bit tricky with let generalization (which is why it's generally mixed). Have you ever play with prolog? Prolog uses unification to run programs. ?- f(X) = f(Y). X = Y. You can basically pass these equations to prolog and i'll solve it for you ?- A = int, B = array(A), C = B. A = int, B = C, C = array(int). (Don't quote me on that though. I'm still new to prolog) icefox — Today at 2:52 PM I've played with Prolog but not in a loooong time
Comment by ~icefox on ~icefox/garnet
More user experiences with QBE: https://briancallahan.net/blog/20210829.html This post got me thinking more about what I actually want to do. Current loose plans:
- Currently,
garnetccompiles to Rust. This Is Fine.- When
garnetcself-hosts, it will be designed to have multiple backends. This may or may not be a stable API, but should be relatively consistent and easy to get going.- The end goal for instruction sets to support will be amd64, arm32, aarch64, riscv32, riscv64, wasm32, and wasm64 once it exists. 32-bit x86 would also be nice but IMO adds relatively little value right now; it's not common on desktops, not common on mobile hardware, and not common in embedded hardware. Maybe a compelling reason to support it will show up.
- I would also like to have a backend that generates C code. This isn't strictly necessary but would be kinda nice for portability: instead of distributing bootstrap binaries you could generate and distribute portable C code, compile it with a C compiler, and then use the resulting
garnetcto bootstrap itself from the Garnet sources. A little ironic, considering my goal is to make C entirely obsolete, but still it sounds neat.- So, once the compiler is self-hosted, having a QBE backend and a C backend would get us most of these targets. Contributing a wasm backend to the QBE codebase sounds like it would probably not be horrible, and would be good for everyone.