~icefox

Just foxing about.

https://wiki.alopex.li/

Trackers

~icefox/garnet

Last active 16 days ago

~icefox/oorandom

Last active 9 months ago

~icefox/scalar

Last active 1 year, 5 days ago

~icefox/cf_issues

Last active 2 years ago

#30 Assertion fail in typeck 16 days ago

on ~icefox/garnet

REPORTED RESOLVED FIXED

#30 Assertion fail in typeck 16 days ago

Comment by ~icefox on ~icefox/garnet

#15 Refactor errors some 16 days ago

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.

#17 Thoughts on type metaprogramming 17 days ago

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.

#17 Thoughts on type metaprogramming 17 days ago

Comment by ~icefox on ~icefox/garnet

Related: https://github.com/fsharp/fslang-suggestions/issues/243

How does F# handle this sort of thing, anyway?

#31 Formal type system notes 17 days ago

Comment by ~icefox on ~icefox/garnet

Related: #1

#31 Formal type system notes 20 days ago

T-DESIGN added by ~icefox on ~icefox/garnet

#31 Formal type system notes 20 days ago

Ticket created by ~icefox on ~icefox/garnet

Bidirectional type checking:

System F stuff:

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

#22 Thoughts on backends 27 days ago

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, garnetc compiles to Rust. This Is Fine.
  • When garnetc self-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 garnetc to 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.

#30 Assertion fail in typeck a month ago

T-BUG added by ~icefox on ~icefox/garnet