hitchhiker's guide

Stream: new members

[Nam]

is the palindrome proposition in hitchhiker's guide... wrong? how would it work with even-length palindromes?

[Nam]

inductive palindrome {α : Type} : list α → Prop
| nil : palindrome []
| single (x : α) : palindrome [x]
| sandwich (x : α) (xs : list α) (hxs : palindrome xs) :
palindrome ([x] ++ xs ++ [x])

[Kevin Buzzard]

[] has even length

[Nam]

ahhh, i see where i got it wrong now. the sandwich constructor sandwiching a list

[Nam]

i read it wrongly to be two lists sandwiching an element

[Jasmin Blanchette]

Kevin, for a mathematician, your mastery of C.S. topics is astonishing.

[Kevin Buzzard]

Once I remember an undergraduate asking me if zero was an even number

[Kevin Buzzard]

The alternative being that the predicate only made sense on positive integers

[Jasmin Blanchette]

The Ancient Greeks didn't like division by 1, I'm told. They would write things like "if n = 1, then m; otherwise m / n".

[Aniruddh Agarwal]

Thereby allowing division by 0? :grinning_face_with_smiling_eyes:

[Reid Barton]

Division by what now?

[Nam]

def action (σ α : Type) := σ → α × σ
def diff_list : list N → action N (list N)
#eval diff_list [1, 2, 3, 2] 0

#. why is the body of the first def, erm, kinda weird? it is a function type.
#. diff_list has one argument, why do we call it with 2 (a list, and the initial state)? is this the first argument (\sigma) in action?

[Mario Carneiro]

action is defining a type, which is a function type in this case

[Mario Carneiro]

the type of action is action : Type -> Type -> Type

[Mario Carneiro]

diff_list has one argument, but the result is an action, which is itself a function, expecting an argument of its own (the sigma, as you say)

[Nam]

so the first def is like a typedef in C?

[Nam]

is there a keyword for that? say, alias?

[Mario Carneiro]

def is like typedef indeed. There is no separate keyword, as in DTT the operations of making a type and making a term are the same

[Nam]

def action.pure {σ α : Type} (a : α) : action σ α
def action.bind {σ : Type} {α β : Type} (ma : action σ α) (f : α → action σ β) : action σ β

@[instance] def action.lawful_monad {σ : Type} :
lawful_monad (action σ) :=
{ pure := @action.pure σ,
bind := @action.bind σ,
...

how should I read the @action.pure \sigma? action.pure does not take a type, does it?

[Mario Carneiro]

action.pure takes three arguments: σ α and a, but normally the first two are inferred because they are written in {} binders. When you use @action.pure they all become explicit, and so it's expecting three arguments. If you only provide the first, that is, σ, you get a function waiting for the other two arguments

[Mario Carneiro]

(and actually, if I recall the definition of action from your last question, there is another argument hidden inside the definition of action itself, so you can actually put four arguments in before you get a value.)

[Nam]

i see. thank you!

[Nam]

speaking of my previous questions, it was something like this.

def diff_list : list N → action N (list N)
...
#eval diff_list [1, 2, 3, 2] 0

[Nam]

which brings me to another question. diff_list [1, 2, 3, 2] returns an action, which is \sigma -> \alpha \times \sigma, which is a function

[Mario Carneiro]

You should be able to do something similar with pure:

#eval @action.pure N (list N) [1,2,3] 0
-- (0, [1,2,3])

note that I passed 4 arguments to pure

[Nam]

so do i get it right that #eval diff_list [1, 2, 3, 2] won't do much?

[Mario Carneiro]

it's a curried function, so no, it might do some computation but it's still waiting for an argument

[Nam]

def diff_list : list N → action N (list N)
| [] := pure []
...

why do i not have to specify action.pure? how does lean know if the pure [] is for action and not, say, set? is that because it is matched with the return type?

[Nam]

but which type is right? which declaration takes precedence? the signature, or the code in the body?

[Mario Carneiro]

pure is not actually the same function as action.pure, it is the pure function from the root namespace. This function has a typeclass argument allowing it to work on anything with a monad instance, and your @[instance] def action.lawful_monad registered action.pure as the pure operation of the action monad

[Mario Carneiro]

It knows to look for the monad instance on action and not set because the expected return type of pure [] is action N (list N)

[Mario Carneiro]

Nam said:

but which type is right? which declaration takes precedence? the signature, or the code in the body?

Elaboration in lean proceeds outside-in, from the expected type down to the types of variables. So the signature is always taken verbatim unless it is not provided (and you are required to provide it at the top level of a definition by cases like that one).

[Mario Carneiro]

If lean didn't know the expected type, it wouldn't be able to figure out what pure [] means in this instance

[Mario Carneiro]

For example,

def diff_list : list nat → state nat (list nat)
| _ := let x := pure [] in x

fails because I haven't said what type x is

[Nam]

Mario Carneiro said:

For example,

def diff_list : list nat → state nat (list nat)
| _ := let x := pure [] in x

fails because I haven't said what type x is

could you elaborate why it fails? my guess is at the let declaration, x type is not known. but shouldn't the return type be propagated backward because that same x is returned?

[Mario Carneiro]

When lean elaborates a let expression, it first tries to elaborate the let definition, and then only if that is successful, uses the result in the body. This is done mostly to localize error reporting, but it does prevent it from finding the solution in this case, even though the information is available in principle

[Jake]

"Dependent types often make definitions and proofs more difficult". My prior intuition was the opposite, i thought being more precise means the compiler could help you out more, and code generation / simplification is better. Can someone explain what the author means by difficult here?

[Johan Commelin]

You can do more stuff. The new stuff is hard.

[Johan Commelin]

That's a very brief summary.

[Johan Commelin]

For evidence of the pain, search the history of this chat for "motive is not type correct".

[Patrick Massot]

I think the author means he's more used to Isabelle.

[Mario Carneiro]

More dependent types means more arguments to functions across the board, so it's not necessarily the case that code performance improves

[Reid Barton]

Hard to guess what the author had in mind with so little context.

[Mario Carneiro]

simplification is much harder because of complicated definitional equality problems that can come up at any point

[Reid Barton]

for example, more difficult than what: programming without dependent types, or theorem proving without dependent types?

[Mario Carneiro]

and there are a number of constructions that would be convenient to do in a proof that are only type correct up to a propositional equality, and these require the insertion of "cast" functions into the term that later obstruct simplification and other kinds of term analysis

[Mario Carneiro]

that is a slightly less brief summary of "DTT hell"

[Mario Carneiro]

Dependent types can enhance a programmatic proof with invariants and such without adding any additional overhead, when everything goes well and things fit together nicely. But when things don't work out exactly right, the fallback is much worse than the simply typed scenario

[Mario Carneiro]

I think Conor McBride has a number of papers on what DTT looks like on a good day

[Anne Baanen]

I've changed the sentence to: "Dependent inductive types often cause difficulties when the terms they depend on don't line up nicely.", basically what @Mario Carneiro says.

[Jasmin Blanchette]

And I've edited it further with an example in parentheses (m + n vs. n + m).