Alice ✨

@welltypedwit.ch

There’s no sense crying over every mistake. You just keep on trying ’til you run out of cake - GLaDOS https://welltypedwit.ch

$pub unsafe fn boxed_element(&self, index: usize) -> *const u8 { debug_assert!(index > 0 && index < self.layout.boxed_count); // In objects at-rest, boxed elements are stored first. // See Note [At-rest vs in-flight] in src/Vega/Compilation/LLVM/Layout.hs$

the same code with a

_: *const HeapObject = heap_object_pointer

that shows an error under heap_object_pointer

let heap_object_pointer = object.byte_sub(HeapObject::HEADER_SIZE_IN_BYTES);
heap_object_pointer as *const HeapObject

there is an inlay hint that heap_object_pointer ostensibly has type *const HeapObject

thread '<unnamed>' (172361) panicked at src/heap.rs:31:22:
misaligned pointer dereference: address must be a multiple of 0x8 but is 0x564040da86f9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

diff swapping the order of argumetns to LLVMBuilder.buildStore

diff swapping the arguments to LLVMBuilder.buildMemCpy

%unboxed = alloca [16 x i8], align 512
store i64 %z_7, ptr %unboxed, align 512

llvm declaration for a vega function that takes and returns an i512

~100 error messages about various types not matching type 'a', followed by:

ERROR: PANIC (the 'impossible' happened): Skolem corresponding to a non-parameter representation type variable found while trying to convert representations to core. This should not have happened!
Skolem: r$a

ERROR: PANIC (the 'impossible' happened): unsubstituted type variable in unification: MkLocalName {parent = MkDeclarationName {moduleName = MkModuleName {package = MkPackageName "meridian", subModules = fromList ["Route"]}, name = "executeWith"}, name = "r$matchData", count = 0}:

before: rss: 843.56640625, heapUsed: 753.8318328857422
after: rss: 767.37890625, heapUsed: 677.5433197021484

let lol = []

function leakyBoi() {
let array = []
for(let i = 0; i < 1024*1024*4; i++) {
array.push(i)
}
lol.push(() => array[69])
}

for (let i = 0; i < 20; i++) {
leakyBoi()
}
console.log(`before: rss: ${Deno.memoryUsage().rss / 1024 / 1024}, heapUsed: ${Deno.memoryUsage().heapUsed / 1024 / 1024}`)
lol = []
globalThis.gc()
console.log(`after: rss: ${Deno.memoryUsage().rss / 1024 / 1024}, heapUsed: ${Deno.memoryUsage().heapUsed / 1024 / 1024}`)

rust foundation sponsor page for "Helsing", joined july 2023:

Helsing is a pan-European, multi-domestic defense company with national entities in Germany, the UK, and France. They believe that software, in particular artificial intelligence, will be the key to protecting democracy. Their teams design technology products that transform the operational capabilities of both new and existing defense platforms, to deliver faster and more accurate decision-making at the tactical, operational, and strategic levels. Approximately 50% of Helsing’s code is Rust-native and the other half is slowly but surely getting replaced with Rust.

def P := 5
def NP := 4
def AI := 1

def p_equals_NP : P = NP + AI := by
rfl

main : () -> ()
main() = {
let list = ArrayList.newWithCapacity(3)
ArrayList.push(list, 65u8)
ArrayList.push(list, 66u8)
ArrayList.push(list, 67u8)
ArrayList.push(list, 68u8)
ArrayList.push(list, 69u8)
ArrayList.push(list, 70u8)
ArrayList.push(list, 71u8)
ArrayList.push(list, 72u8)
ArrayList.push(list, 73u8)
-- ArrayList.push(list, 74u8)
-- ArrayList.push(list, 75u8)
-- ArrayList.push(list, 76u8)
print(String.fromByteArray(ArrayList.freeze(list)))

85
most followers: 80
most posts per day: 91
most liked posts: 96
biggest reply guiy: 78
longest posts: 82

vscode minimap where almost everything is red

git pull text thingy showing 187(!!) files changed, 2051 insertions, 444 deletions

vega panic "Non-record type in record field access" showing what is clearly a record type

-- type: compile

f : { g : forall (a : Type(Boxed)). a -> a } -> forall (a : Type(Boxed)). a -> a
f(record) = record.g

main : () -> ()
main() = {}

$import internal:Internal (intToInt32, emptyArray) import std:IO/Posix/FileDescriptor (stderr) import std:IO/Posix (print, printFD) import std:String (append) import meridian:Error (fatalError, handleNegative) import meridian:Socket (Socket, createTCP, bindTCP, listen, accept) import meridian:Parser (makeParser, parseRequest) import meridian:Request (Request) import meridian:Response (Response, sendResponse) import meridian:Meridian (run) main : () -> () main() = { run({ port = 3000u16, onRequest = \request -> { Response({ headers = emptyArray(), status = 200, statusMessage = "OK", body = "<h1>OMG IT WORKS</h1>", contentType = "text/html" }) } }) }$

diff changing

let path = [MIR.SumConstructorPath index, MIR.ProductFieldPath productIndex]

to

let path = case parameters of
-- If the constructor only has a single parameter, we don't have an internal product
[_] -> [MIR.SumConstructorPath index]
_ -> [MIR.SumConstructorPath index, MIR.ProductFieldPath productIndex]

invocation of VEGA_TRACE=coreToMIR vega build where there are several more declarations being compiled after meridian:Parser:parseUntilSpace before showing a compiler panic

-- | The offset of the actual array contents from the start of the object data (just *after* the header)
arrayContentOffset :: Int
arrayContentOffset = 8

-- Arrays are represented as pointers to their contents so unsafeArrayContents doesn't actually need to do anything

vega MIR for the same function but this time it only uses a single unbox operation and unboxes it at the correct representation (IntRep * ArrayRep($0) * IntRep * ArrayRep($0) * IntRep)

MIR VERIFICATION ERROR: Trying to access non-product representation Boxed with a ProductConstructorPath.
In path access for sourceOffset_2 accessing [ProductFieldPath(0)] on Boxed
MIR VERIFICATION ERROR: Trying to access non-product representation Boxed with a ProductConstructorPath.
In path access for targetArray_4 accessing [ProductFieldPath(1)] on Boxed
MIR VERIFICATION ERROR: Trying to access non-product representation Boxed with a ProductConstructorPath.
In path access for targetOffset_6 accessing [ProductFieldPath(2)] on Boxed
MIR VERIFICATION ERROR: Trying to access non-product representation Boxed with a ProductConstructorPath.
In path access for sourceArray_8 accessing [ProductFieldPath(3)] on Boxed
MIR VERIFICATION ERROR: Trying to access non-product representation Boxed with a ProductConstructorPath.
In path access for length_10 accessing [ProductFieldPath(4)] on Boxed

vega MIR code that unboxes the same closure 5(!!) times, always unboxes it at representation Boxed and then tries to access fields on it

part of the typing rules from https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/putting.pdf (not very, accessible sorry)
where the |- ... <= ... judgement (subsumption) elaborates to a term f that inserts a bunch of lambdas and applications depending on the types

vega error message:
Inaccessible type constructor Pointer
The following definitions are available but not imported:
- internal:Internal:Pointer

10 ┃ external puts : Pointer(UInt) -> ()

(in vega):
$ find test -name "*gay*" | count
0

$define tailcc void @"_vega_test::Main::blah[I,I]"(ptr sret([24 x i8]) align 8 %0, ptr byval([16 x i8]) align 8 %1, ptr byval([24 x i8]) align 8 %2) { br label %4 4: ; preds = %3 %tagptr = getelementptr inbounds i8, ptr %2, i64 23 %tag_2 = load i8, ptr %tagptr, align 1 switch i8 %tag_2, label %unreachable [ i8 0, label %5 i8 1, label %8 ] 5: ; preds = %4 %_3 = alloca [24 x i8], align 8 %6 = getelementptr inbounds i8, ptr %_3, i64 23 store i1 false, ptr %6, align 1 %7 = getelementptr inbounds i8, ptr %_3, i64 0 call void @llvm.memcpy.p0.p0.i64(ptr align 8 %0, ptr align 8 %_3, i64 24, i1 false) ret void 8: ; preds = %4 %9 = getelementptr inbounds i8, ptr %2, i64 0 %x_5 = load i64, ptr %9, align 4 %10 = getelementptr inbounds i8, ptr %2, i64 8 %x235_6 = load ptr, ptr %10, align 8 %11 = alloca [24 x i8], align 8 call void @llvm.memcpy.p0.p0.i64(ptr align 8 %11, ptr align 8 %x235_6, i64 24, i1 false) %12 = getelementptr inbounds i8, ptr %1, i64 0 %13 = load ptr, ptr %12, align 8 %14 = getelementptr inbounds i8, ptr %1, i64 8 %payload = load ptr, ptr %14, align 8 %x236_8 = call tailcc i64 %13(i64 %x_5, ptr %payload) %x237_9 = alloca [24 x i8], align 8 call tailcc void @"_vega_test::Main::blah[I,I]"(ptr sret([24 x i8]) align 8 %x237_9, ptr byval([16 x i8]) align 8 %1, ptr byval([24 x i8]) align 8 %11)$

$test:Main:blah(f_0 : (FunctionPointer * Boxed), x_1 : (Unit + ($0 * Boxed))) : (Unit + ($1 * Boxed)) = { init: 249 blocks: 249: tag_2 = loadSumTag x_1 switchInt tag_2 [ 0 -> 250 1 -> 251 ] 250: _4 = product () : Unit _3 = sum [0](_4) : (Unit + ($1 * Boxed)) return _3 251: x_5 = accessField [SumConstructorPath(1)->ProductFieldPath(0)] x_1 : $0 x235_6 = accessField [SumConstructorPath(1)->ProductFieldPath(1)] x_1 : Boxed xs_7 = unbox x235_6 (Unit + ($0 * Boxed)) x236_8 = callClosure f_0(x_5) x237_9 = callDirect test:Main:blah[$0, $1](f_0, xs_7) x238_10 = box x237_9 _12 = product (x236_8, x238_10) : ($1 * Boxed) _11 = sum [1](_12) : (Unit + ($1 * Boxed)) return _11 }$

reddit comment with 13 upvotes:

> you could use rust if you were happy with lots of unsafe code

Using C++ kinda implies that you are

cohost post from @prophet (me). the tags appear after the content of the post in a smaller, slightly faded font

voice training tip: mantra phrases are useful because if you do them often enough they'll grant you divinity and you'll deal triple damage send chost

#voice training but not really #slay the spire

data AdditionalParseError
= MismatchedFunctionName
{ loc :: Loc
, typeSignature :: Text
, definition :: Text
}
| NonVarInFunctionDefinition Loc
| InvalidExistentialBinder (ForallBinderS Parsed)
| NonLiteralMultiplication {loc :: Loc}
deriving stock (Eq, Ord, Generic)
deriving anyclass (HasLoc)

there is a pink box around UnknowNamedKind's definition

function buildFlat(size) {
let list = { tag: "Nil" }
for (let i = 0; i < size; i++) {
if (i % 2 == 0) {
list = { tag: "Cons1", head1: i, tail1: list }
} else {
list = { tag: "Cons2", head2: i, extra: i * i, tail2: list }
}
}
return list
}

function sumFlat(list) {
switch (list.tag) {
case "Nil":
return 0
case "Cons1":
return list.head1 + sumFlat(list.tail1)
case "Cons2":
return list.head2 + sumFlat(list.tail2)
}
}

screenshot of a post where the image doesn't load and it only shows the alt text

function buildFlat(size) {
let list = { tag: "Nil" }
for (let i = 0; i < size; i++) {
list = { tag: "Cons", head: i, tail: list }
}
return list
}

function sumFlat(list) {
switch (list.tag) {
case "Nil":
return 0
case "Cons":
return list.head + sumFlat(list.tail)
}
}

throughput:

flat ({ tag: "Cons", head: ..., tail: ... } / { tag: "Nil" }): 75905 ± 0.17%
padded ({ tag: "Cons", head: ..., tail: ... } / { tag: "Nil", head: 0, tail: null }): 81735 ± 0.13%
payload object ({ tag: "Cons", payload: { head: ..., tail: ... } } / { tag: "Nil", payload: {} }): 55423 ± 0.20%
payload array ({ tag: "Cons", payload: [..., ...] } / { tag: "Nil", payload: [] }): 48729 ± 0.18%
array ([1, ..., ...] / [0]): 59473 ± 0.16%
padded array ([1, ..., ...] / [0, 0, null]): 59306 ± 0.15%

$pattern BindMatch :: forall (n :: Nat) (m :: Nat). (KnownNat n, n ~ m) => (n ~ m) => BitString -> Match n pattern BindMatch bitstring <- Match bitstring parseBinaryProtocol :: forall (bytes :: Nat) -> KnownNat bytes => BitString -> IO () parseBinaryProtocol bytes = \case Match @16 checksum :| BindMatch @8 @payloadBytesSize payloadBytes -- :| Match @payloadBytesSize -- doesn't work because this would try to *bind* a second payloadBytesSize type variable (and fail) :| Match @8 payload :| _rest -> undefined _ -> undefined$

Error message for

newtype Match (n :: Nat) where
Match :: forall (n :: Nat) -> BitString -> Match n

Illegal visible, dependent quantification in the type of a term

$type BitString = [Bool] newtype Match (n :: Nat) = Match BitString pattern (:|) :: forall n. (KnownNat n) => Match n -> BitString -> BitString pattern match :| rest <- (matchBitString n -> Just (match, rest)) infixr 5 :| pattern End :: BitString pattern End = [] matchBitString :: forall (n :: Nat) -> (KnownNat n) => BitString -> Maybe (Match n, BitString) matchBitString n bitstring | length bitstring < sizeMatched = Just (Match (take sizeMatched bitstring), drop sizeMatched bitstring) | otherwise = Nothing where sizeMatched = fromInteger $ natVal (Proxy @n) parseDNSPacked :: BitString -> IO () parseDNSPacked = \case Match @16 id :| Match @1 qr :| Match @4 opcode :| Match @1 aa :| Match @1 tc :| Match @1 rd :| Match @1 ra :| Match @3 z :| Match @4 rcode :| Match @16 qdcount :| Match @16 ancount :| Match @16 nscount :| Match @16 arcount :| End -> undefined _ -> fail "invalid dns packed"$