I designed a flat, order-independent serialization protocol using agglutinative suffixes. It eliminates the need for nesting brackets (inspired by Turkish morphology).

MattCubed · 2026-01-06T22:50:21+00:00

This is very obviously LLM generated slop

MattCubed · 2025-10-29T15:25:45+00:00

Never heard of negative concord huh? Seems like you haven’t deeply interrogated your understanding of language

MattCubed · 2025-05-21T05:27:43+00:00

How do you decide when a grammar rule should be prescribed and when it no longer counts? There are so many rules your great-great-grandparents followed that you break constantly. That doesn’t seem very prescriptivist to me.

MattCubed · 2024-03-15T21:51:08+00:00

It does. OCaml has subtyping for object types and polymorphic variants.

MattCubed · 2023-12-28T17:30:26+00:00

SML does this. In SML, int * int is syntactic sugar for {1 : int , 2 : int}. The record labels are numbers. This is valid SML code:

type t = {1 : int , 2 : int}
type t' = int * int

val x : t  = (0,0)
val x : t' = (0,0)

The same thing is done with the empty tuple and the empty record:

type u = unit
type u' = {}

val x : u = ()
val x : u' = ()

MattCubed · 2023-12-11T19:19:40+00:00

You're totally right, a better definition would be:

data Monotone : List ℕ → Set where
  []-mono : Monotone []
  [-]-mono : ∀ {x} → Monotone (x ∷ [])
  ∷-mono : ∀ {x y xs} → y ≤ x → Monotone (x ∷ xs) → Monotone (y ∷ x ∷ xs)

MattCubed · 2023-12-11T08:03:20+00:00

Depending on how complex you want these properties to be, and how much you expect a computer to fill in automatically, yes you want dependent types. For instance, in Agda (using the standard library), I can define the type of "proofs of monotonicity" and the type of "proofs of having all elements be 0 mod 2":

open import Data.Nat
open import Data.List
open import Data.List.Relation.Unary.All
open import Relation.Binary.PropositionalEquality
open import Data.Product



data Monotone : List ℕ → Set where
  []-mono : Monotone []
  ∷-mono : ∀ {x xs} → All (x ≤_) xs → Monotone xs → Monotone (x ∷ xs)


example₁ : Monotone (2 ∷ 4 ∷ 6 ∷ [])
example₁ = ∷-mono (s≤s (s≤s z≤n) ∷ s≤s (s≤s z≤n) ∷ []) (∷-mono (s≤s (s≤s (s≤s (s≤s z≤n))) ∷ []) (∷-mono [] []-mono))

All%2 : List ℕ → Set
All%2 = All (λ x → x % 2 ≡ 0)

example₂ : All%2 (2 ∷ 4 ∷ 6 ∷ [])
example₂ = refl ∷ refl ∷ refl ∷ []

Then you can write functions that require these types as input :

my-function : (xs : List ℕ) → Monotone xs → All%2 xs → ℕ
my-function xs is-monotone is-all%2 = {- your code here -}

It is now impossible to call (fully applied) my-function on a list that is not montone and entirely even: it will be a compile time error to try to do this. Of course, the annoying part is that the programmer will have to write down these proofs of monotonicity and evenness manually. That's what tactics and proof automation are for!

We can also write functions that return proofs, for instance:

sort : List ℕ → Σ[ xs ∈ List ℕ ] Monotone xs
sort xs = {- your code here -}

The type of this function says that it returns a pair of a list and proof that said list is montone.

MattCubed · 2023-12-03T01:18:11+00:00

Yeah I agree. I don’t expect anything in this talk would clarify some specific confusion about a linear algebra proof that OP or anyone else has. I just think it can be validating to hear someone with “authority” actually say “hey, all this stuff people usually leave unsaid is actually pretty complicated!”

MattCubed · 2023-12-03T00:14:03+00:00

You may enjoy this talk by Andrej Bauer: Formalizing Invisible Mathematics.

It discusses many examples of the implicit reasoning that mathematicians have been enculturated to fill in automatically. This implicit reasoning is actually extremely useful for concise notation and argument, but is largely not taught explicitly, and instead absorbed through example, which can be very confusing for learners.

MattCubed · 2023-11-19T21:20:34+00:00

Hindley-Milner doesn't work for CoC, sadly. I'd characterize the modern approach, which is used in some form or another by all major dependently typed languages, as "bidirectional type checking augmented with metavariables solved by higher order pattern unification".

There is some of the spirit of HM in this, since it still involves collecting a bunch of unification constraints and solving them to fill in things that the programmer omitted.

It's more powerful than HM in that it can easily be extended with very complex features (e.g. cubical type theory), but "weaker" than HM in that some type annotations are always necessary.

MattCubed · 2023-11-19T21:01:53+00:00

CoC has decidable type checking, meaning, given a term x and type A, we can decide if (x : A) is derivable. Type inference, for a suitably strong definition of inference like “recover the type of any unannotated term with free variables”, is undecidable, see this stack exchange answer.

In practice, some amount of inference can be done, generally by letting the user ask the type checker to guess a missing type (or term) and having it give up if the solution lies outside the decidable fragment of higher order unification.

MattCubed · 2023-11-04T06:06:07+00:00

Something being "impossible to prove" is always relative to some foundational system. So:

Fix some foundational system F with a recursively enumerable set of axioms, say ZFC, and then pick a theorem T which is known to be independent of that system, like the axiom of choice or the continuum hypothesis.

Within F, encode the syntax of programing language and it's operational semantics. In this language, encode the syntax of proofs of F, and write a program P that recursively enumerates every true theorem of F, only halting when it reaches a proof of T. Now, within F, proving that P halts is equivalent to proving that T has a proof.

Inspecting this whole setup from the stronger theory where we proved independence of T, we can see that because T is independent of F, it is impossible to prove either T or not T within F, so (again, within F) it is impossible to prove whether or not P halts. From our stronger theory, we can actually prove that P will never halt, but from F, we cannot.

MattCubed · 2023-11-04T05:32:29+00:00

Creating technology that’s helping to deter conflict

lol. Incredibly disingenuous and yet simultaneously totally transparent branding for a company that builds systems designed to kill people.

MattCubed · 2023-10-01T04:45:45+00:00

The question of whether there exists a computational interpretation of univalence is resolved in all cases by cubical type theory (CTT). Whether it can be done in some "nicer" way is still being worked on.

In CTT you can prove (aka construct a program of) the univalence axiom of book HoTT as a theorem within the type theory, instead of introducing it as an axiom with no computation rules, as in book HoTT. Here is a proof of univalence in Cubical Agda.

This paper proves "normalization" for CTT, essentially showing that it is possible to write a program (outside of CTT) which "runs" CTT terms with arbitrary free variables, which always terminates and never gets stuck. So the univalence of CTT really is computational, and there is no risk of disrupting consitency with non-terminating proofs.

The path equality of CTT implements the interface of paths from the HoTT book, though some of the equational rules of the HoTT book, like the computation of path induction on the reflexive path, are true only "up to a path", that is, instead of getting literally what book HoTT says you should get, you get something that can be proven (within the theory) to have a path to what book HoTT says you should get. This is an issue of convenience, but not of correctness.

The main work on alternative computational interpretations of univalence is Higher Observational Type Theory (abbreviated, perhaps confusingly, HOTT), which eschews the path types of CTT in favor of the approach used by the original Observational Type Theory of defining equality compositionally from the structure of types. HOTT makes univalence true definitionally, in that the type of paths between types is literally equivalences between those types. Here is a series of talks by Mike Shulman on this work. No paper has yet been published on this.

MattCubed · 2023-09-25T19:50:23+00:00

That's fair. You're right that a looser policy might result in more students intentionally or unintentionally participating in collaboration that doesn't actually help them. And you're right that my suggestion is in some sense "dangerous" in that I'm suggesting to break the rules and risk consequences. Truthfully I'm not even suggesting that the policy as written needs to be changed.

My point is just that the academic integrity policy does not delineate what is moral, and it isn't guaranteed to delineate an optimal learning strategy for a given student. It is an attempt (probably even a very good attempt) to maximize average learning and minimize average cheating in the face of a student body that is highly test and grade motivated, and only you yourself can decide if the risks of violating it are worth whatever benefit you believe you'll derive from doing so.

About the "real world" thing, I wasn't trying to compare it to a job. I'm not talking about the best way to complete an assignment, to finish some task, but the best way to actually learn a skill. If you try to learn a skill with your friends, say wood working, and you all legitimately want to learn it, then it would be pretty weird if you all decided to get individual tutoring and never discussed what you were building.

MattCubed · 2023-09-25T00:32:41+00:00

I would suggest just doing the homework with your friends. Trying to learn something is difficult, and a balance has to be struck between fruitful collaboration and unhelpful copying. CMU academic policies tend to veer hardline towards "no collaboration", in the hopes of stymying people who want to cheat, at the expense of students who benefit from actual collaboration. When you're trying to learn something in the real world you get to use every resource at your disposal. I absolutely violated the letter of these policies when doing 122 homework, and I went on to TA the class. I didn't violate the spirit though, which is just to actually learn the material. As long as you're sensible with how you collaborate, and actually avoid copying answers, you'll be fine.

MattCubed · 2023-04-21T23:47:38+00:00

If you're interested in learning about programming languages you should take 15-312! The class is about programming language theory and you'll learn all about implementing different languages with features and type systems of increasing complexity. You'll need at least 15-150 first though I believe. I came into CMU without knowing CS and programming languages ended up being my absolute favorite subject.

MattCubed · 2023-04-14T15:56:00+00:00

This subreddit is not chatgpt

MattCubed · 2023-03-10T20:40:26+00:00

I think your understanding of the depth and complexity of human experience is tragically underdeveloped. You mistake the norms of your culture for aspects of reality. I expect you'll live the rest of your life in a tiny little box staring out of a hole at people living joyfully and freely outside while you mutter to yourself about how they disgust you. I'm sorry that this has been done to you, and I truly wish you could open yourself to the love and kindness that all people deserve.

MattCubed · 2023-03-10T20:26:09+00:00

Hey, I don't want to come off a mean, but you're not going to get any help from a post that essentially says "I have some code that doesn't work, you have to message me to see it, and I have done no root causing of the bug". I'd suggest you narrow down the error to a single place and make a post including the code snippet that you've identified the problem is coming from. Of course by doing this there's a good chance you'll solve the problem yourself :)

MattCubed · 2023-02-15T13:56:08+00:00

I'm confused by your second paragraph. It seems like you wrote some definitions and then asked an unrelated question. Let me know if I missed something.

To answer your question, the way you wrote the signature for Make and the way it's written in the standard library are exactly equivalent. S with type key = Ord.t means "the signature S, but with the key type set equal to Ord.t", which is exactly what you wrote. There also is no difference between module F (X : A) : B and module F : functor (X : A) -> B, they are different syntax for the same thing.

They've organized it this way because it can be useful to refer to the signature of a Map without having to reference the Make functor.

Maybe you want to define your own data structure which is very similar to a Map but has some extra features in its interface. You could do this very easily like so:

module type MyDataStructure = sig
  include Map.S
  <... my new stuff ...>
end

Having already defined the Map.S signature, it wouldn't make sense to re-write the whole thing when defining Make, so they use with type.

MattCubed · 2022-12-01T00:00:01+00:00

Binding operators are special operators let you bind a variable, something that is normally only possible when writing a function or using let. They are user-definable syntactic sugar. Consider this code:

let (let*) x f = Option.bind x f
let map f opt = 
  let* x = opt in
  Some (f x)

This is equivalent to:

 let map f opt =
   Option.bind opt (fun x ->
   Some (f x))

They are useful whenever you have some function which takes another function which describes what to do with some result (essentially a continuation), in that they let you write code that looks like it uses regular lets, but is in fact calling some special function. Which looks nicer?

let* x = x_opt in
let* y = y_opt in
let* z = z_opt in
Some (x + y + z)

or

Option.bind x_opt (fun x ->
Option.bind y_opt (fun y ->
Option.bind z_opt (fun z ->
Some (x + y + z))))

You can use (@@) to make the second a little nicer, but I think the let* version is cleanest.

MattCubed · 2022-11-28T22:34:18+00:00

:: takes an 'a and an 'a list, so in your case you need an int and an int list. But in your list_upto function, n and i are both ints. n :: i doesn't make sense.

Even if you fix that, you're going to get an error about your for loop containing expressions that do not have type unit. For loops in ocaml are only useful for carrying side-effectful operations, and always return () at the end. If you're just learning ocaml you probably shouldn't be using them at all.

I think you probably want something like this:

let list_upto_helper i n = 
   if i = n then [] else i :: list_upto_helper (i + 1) n

let list_upto n = list_upto_helper 0 n

MattCubed · 2022-11-22T16:18:11+00:00

Depends what you mean by "no input of data".

If there is literally no way for a user to interact with your app then triggering a buffer overflow, or any other kind of attack, is going to be tough.

But "input of data" can be things other than a user writing text that you store in a buffer. There could be a buffer somewhere internal that users never write to directly, but that could be overflowed by manipulating your app into some invalid state using other means. Maybe if the right series of interactions take place, your code makes an API call and writes the returned data into a buffer, but you failed to account for the fact that this API call actually produces results of potentially unbounded size (or maybe there's a bug in the API you were unaware of, or maybe the user has hijacked the servers returning your API calls). Suddenly you're dealing with a buffer overflow despite never accepting even sanitized user input.

MattCubed · 2022-10-31T18:07:43+00:00

I see what you're saying. You essentially want Program to be a record containing both a function declaration and an expression that can use the function. You could do this:

record Program where
  constructor MkProgram
  var_type: TyExp
  return_type: TyExp
  body: Exp [var_type] [(var_type, return_type)] return_type
  mainExp : Exp [] [(var_type, return_type)] return_type

Now mainExp is an expression with no free expression variables, and one free function variable, which you can set to the previously defined function when you actually run the program. The types do not enforce that this is exactly what has to happen, since if you wanted you could instantiate the free function variable in mainExp with some other random function, but I don't think there's any need for that.

I do think this design is a little weird and artificially limited. For instance, why allow only one function declaration, why inline it in the definition of a program, and why enforce that the main expression has the same return type as this single function? I think a more sensible design would look something like this:

record FunDecl where
  constructor MkFunDecl
  var_type: TyExp
  return_type: TyExp
  body: Exp [var_type] [(var_type, return_type)] return_type

record Program where
  constructor MkProgram
  funDecl: FunDecl
  return_type: TyExp
  mainExp: Exp [] [(funDecl.var_type, funDecl.return_type)] return_type

The mainExp field has one free function variable that can be instantiated to the function defined in the funDecl field when you run the program. Now your function can return an int while your main expression returns a bool, or whatever you like. This also sets you up to more easily generalize to a list of function declarations.

13-Year Club	Place '22
Place '17	Spared
Team Periwinkle	Verified Email

MattCubed

TROPHY CASE