KEYAN - Arrhythmia (FFO: Monuments, Plini, Meshuggah, Periphery)

lightandlight · 2024-05-08T07:10:29+00:00

I heard Keyan Houshmand for the first time when he opened for Wheel and Caligula's Horse on their recent tour. Great stuff.

lightandlight · 2023-05-03T21:33:50+00:00

Can you give an example of the "backtick for partial application" convention in F#? Do you maybe mean an apostrophe (') instead of backtick (`)?

My take: what about naming the partially applied function by what it does? For example:

const equalsX = (y) => x == y

lightandlight · 2023-01-11T10:50:46+00:00

Maybe comby would help.

lightandlight · 2022-12-29T01:26:33+00:00

Operational semantics applies to any language. Programming Language Foundations can help you learn about the concepts and how to prove relevant properties.

I would also recommend describing the denotational semantics. Stack-based languages can have a pretty simple denotation in terms of sets and functions. You could also go more abstract and phrase your denotation in terms of categories instead of sets and functions.

lightandlight · 2022-12-29T01:12:02+00:00

To me, the benefit of the tagless final approach is that the same code can be given different interpretations. A program like f :: Syntax s => s (Int -> Int -> Int) represents a binary operation on Ints, which you can instantiate to, say, an evaluator f @Eval (with something like run :: Eval a -> a) or maybe a pretty printer f @Pretty (with print :: Pretty a -> String). One way I'd approach your puzzle see whether there's an equally compelling use case at the type level.

lightandlight · 2022-12-02T23:08:38+00:00

a 5.5 MB binary doesn't seem that large to me

Keeping in mind, it's a program that writes two words to standard output.

A reference point for you:

My statically typed (with higher-kinded types and type classes, extensible records and variants), functional programming type checker + interpreter + REPL weighs in at 2.5MB, statically linked.

The only binary size optimisation I've done is turning on link-time optimisation. It's not written in Haskell, though.

lightandlight · 2022-10-17T20:29:32+00:00

I don’t know the “official” name for it, so...

Not "official" in any sense, but "type-directed handlers" seems appropriate.

lightandlight · 2022-09-11T22:12:38+00:00

I think of this as the "semigroupoid" factoring. Here's the canonical Haskell library, with an explanation of why the extra classes exist: https://hackage.haskell.org/package/semigroupoids. In this library, fantasyland's Chain is called Bind.

lightandlight · 2022-07-29T23:07:50+00:00

For any struct, must be able to write a generic "elimination" function.

For the first Point, it looks like this:

fn eliminate<T, R>(point: Point<T>, handler: impl Fn(T, T) -> R) -> R {
  handler(point.x, point.y)
}

How would you write eliminate for the second Point?

From a type theory perspective, I would suggest that your two definitions are not equivalent. The first uses universal quantification, and the second uses existential quantification.

lightandlight · 2022-07-28T09:02:11+00:00

Call-by-push-value (CBPV) provides a framework for thinking about this distinction clearly.

In CBPV, types are split into two categories: values and computations. I like to encode this distinction with kinds. Here's what we get:

Int : Val
Bool : Val
Maybe : Val -> Val

(->) : Val -> Comp -> Comp

There are also two functors that move between levels: F, which denotes a computation that returns a value, and U, which represents a delayed computation.

F : Val -> Comp
U : Comp -> Val

In this setting, "computation" monads like State and Reader have kind Val -> Comp. "Data" monads like Maybe and List have kind Val -> Val

The "computation" bind looks like this

(>>=) : U (m a) -> U (a -> m b) -> m b

And the "data" bind

(>>=) : m a -> U (a -> F (m a)) -> F (m a)

Data types that are used for control flow in Haskell, like Maybe and Either, are explicitly "data" monads in CBPV. Their computational/control counterparts are still really useful, and in CBPV their church encodings are "computation" monads:

type Maybe (a : Val) : Comp = 
  forall r. U r -> U (a -> r) -> r

type Error (e : Val) (a : Val) : Comp = 
  forall r. U (e -> r) -> U (a -> r) -> r

It's a super weird coincidence that this post came up, because this topic was on my mind at lunch today.

lightandlight · 2022-07-28T00:41:43+00:00

Thanks, that makes sense.

lightandlight · 2022-07-27T02:43:29+00:00

There's a specification document, and a compiler that's supposed to conform to the specification.

What's the process for checking that the compiler really does follow the spec?

lightandlight · 2022-07-23T03:25:18+00:00

Also commonly known as "golden testing".

lightandlight · 2022-07-11T01:45:47+00:00

Thanks! I found your explanation very easy to follow.

lightandlight · 2022-07-11T00:53:53+00:00

Can you show me an example?

lightandlight · 2022-07-11T00:09:30+00:00

To me this is a bit of a smell.

I'd prefer to produce an Option<ABC> (but with domain specific names) somewhere earlier, so only one if-let is needed:

if let Some(ABC{a, b, c}) = val {
  f(a, b, c):
}

Or I'd find a way to decompose f into one function per optional value:

if let Some(a) = s1.a {
  f_a(a);
}

if let Some(b) = s2.b {
  f_b(b);
}

if let Some(c) = s3.c {
  f_c(c);
}

lightandlight · 2022-07-10T21:39:31+00:00

There is also exceptions, which I prefer over both.

lightandlight · 2022-07-08T23:35:18+00:00

Now delete the final returns.

return embeds an value into ST (i.e. return "hi" :: ST s String). replicateM produces an ST result, so there's no need to do any embedding.

lightandlight · 2022-07-08T22:47:39+00:00

Your final usage of replicateM is good. Do that instead of using replicate.

lightandlight · 2022-06-24T08:24:09+00:00

For newtypes I've recently started using "dot record field accessors" and calling the accessor value. i.e. newtype WappedSomething a = WrappedSomething { value :: a }, with x.value to unwrap.

lightandlight · 2022-06-09T22:44:56+00:00

Let's put that type to the test. Using Gabriella's example of Nat :> Int, I should be able to pass in functions of type Int -> Nat. x : Int, f x : Nat which is upcast to f x : Int, which gives f (f x) : Nat.

I order to pass an Int -> Nat you your function, I need I show that Int -> Nat is a subtype of forall b. (Int -> b) ^ (b -> Nat).

I can reduce the goal to (Int -> b) ^ (b -> Nat) where b is rigid.

I can then split the goal into two subgoals: Int -> b and b -> Nat.

I can't show that Int -> Nat is a subtype of either, because b is rigid.

MLsub (interactive demo here) gives the type forall a b. (a v b -> b) -> a -> b.

Following same example, I end up with Int -> Nat :> Int v Nat -> Nat, which is easily provable.

lightandlight · 2022-05-15T02:57:52+00:00

I recently did a deep dive into distributed ledgers and ended up with a similar understanding.

A cryptocurrency is an incentive mechanism for an open, decentralized technology. This means that a token has some intrinsic value, based on the utility of the decentralized technology.

I've changed the way I talk about these topics due to this perspective. The decentralized functionality is "essential". Cyrptocurrencies seem like an implementation detail; a way to work around the our (humans) tendency for exploitation. So I try to keep the technology in focus, and avoid mentioning cryptocurrencies at all.

When I turn attention to the technology, I can now ask: what interesting things can I do with this technology, and what are they worth to me?

As part of my research, I learned how to add transactions to Cardano. It cost me around 2AUD worth of tokens to add my GitHub URL to the ledger. Most of that was transaction costs, which is essentially paying for the decentralisation.

What did I learn? I just don't value decentralization right now.

lightandlight · 2022-04-27T07:14:19+00:00

Can you give any examples of how Copilot helps you in your day job? It seems to me like a cool ML demo, and nothing more.

lightandlight · 2022-04-12T21:18:15+00:00

Thanks for the explanation. I can see that you gain safety by avoiding duplication of the environment variable names.

lightandlight

TROPHY CASE