# Learning #2: Gnocchi, Lifting Etiquette, and Idris

This was my first full-ish day in San Francisco. This morning I drove into the city with my parents and they helped me move into my nice little apt downtown. This is my first official “single” in SF. Last year I spent an entire year here and went from a small double in the Tenderloin, to a smaller, shared AirBnb near Alamo Square, to a converted room in lower SOMA. Thus, I am truly on a good trajectory!

Today I was hoping to say I learned some cool things about Agda, however I had some difficulties installing it on my machine (Manjaro) and so I eventually after many different attempts and strategies, gave up. Finally I resorted to trying out Idris, but not until 10PM, so I did not get to far in learning anything interesting. So, this post will cover three, small things I learned today instead of just one.

## Learning 1: Gnocchi is Fantastic

Mind blowing, I know! I had this absolutely wonderful gnocchi with my parents in North Beach this afternoon at a place called The Italian Homemade Company. This gnocchi was doused in Brow Sage Butter and literally melted in your mouth. Quite orgasmic! Below is an image of it stolen from yelp.

## Learning 2: Gym Etiquette is Not Universal

For the seasoned lifter (I guess this is me ?!?) there are a certain set of rules you live by that make your life and the lives of those around you more pleasant. I was surprised to witness a few of these being broken during my first day at Fitness SF. The infractions came against the following two rules:

2. If someone is lifting more than you and is struggling to put back the db’s after a hard set, give them the right of way

Thus today I learned it is a bit more of a free for all here than compared to my gym at school (Colby College) which is predominantly filled with athletes.

## Learning 3: Hello World in Idris

Starting here from scratch, altough I have comtemplated on the first chapter and a half of The Little Typer. What interests me about Idris is it supports Dependent Types. I am not going to pretent I know what these are or even that I have the expectation of understanding them for quite a while. However, this is likely the topic of my thesis next school year, so I am getting an early start.

For those less knowledgable in the dark arts of depedent types (like me), the Intro Documentation for Idris has a nice simple explanation of what I assume to be the basis:

“In conventional programming languages, there is a clear distinction between types and values…In a language with dependent types, however, the distinction is less clear. Dependent types allow types to ‘depend’ on values — in other words, types are a first class language construct and can be manipulated like any other value.”

To Explain this, the intro gives an example of a list. This list is described as:

list n a


Where a is an element type, think type variable in Haskell, and n is the length. Thus, the type here depends on the value…

So to extend this example, they give a function which appends to lists, one of length n and another of length m. This gives the function signature:

app : Vect n a -> Vect m a -> Vect (n + m) a


Absolutely insane, am i rite!

Now something a bit less cool. Below is Hello World for Idris:

module Main

main : IO ()
main = putStrLn "Hello World"


Have I told you yet that this is very Haskell-y?

Anyway, that’s all I have for today! As I said, these learnings will sort of be all over, yet at the same time have an all comprehensive theme (I hope). Until tomorrow!