Zulip Chat Archive

Stream: new members

Topic: hitchhiker's guide


Nam (May 06 2020 at 21:37):

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

Nam (May 06 2020 at 21:37):

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

Kevin Buzzard (May 06 2020 at 21:37):

[] has even length

Nam (May 06 2020 at 21:38):

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

Nam (May 06 2020 at 21:39):

i read it wrongly to be two lists sandwiching an element

Jasmin Blanchette (May 07 2020 at 05:18):

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

Kevin Buzzard (May 07 2020 at 09:28):

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

Kevin Buzzard (May 07 2020 at 09:28):

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

Jasmin Blanchette (May 08 2020 at 15:37):

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 (May 08 2020 at 15:43):

Thereby allowing division by 0? :grinning_face_with_smiling_eyes:

Reid Barton (May 08 2020 at 16:08):

Division by what now?

Nam (May 11 2020 at 01:44):

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 (May 11 2020 at 01:49):

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

Mario Carneiro (May 11 2020 at 01:49):

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

Mario Carneiro (May 11 2020 at 01:50):

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 (May 11 2020 at 02:21):

so the first def is like a typedef in C?

Nam (May 11 2020 at 02:21):

is there a keyword for that? say, alias?

Mario Carneiro (May 11 2020 at 04:08):

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 (May 14 2020 at 02:00):

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 (May 14 2020 at 02:06):

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 (May 14 2020 at 02:07):

(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 (May 14 2020 at 02:08):

i see. thank you!

Nam (May 14 2020 at 02:08):

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 (May 14 2020 at 02:09):

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 (May 14 2020 at 02:10):

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 (May 14 2020 at 02:11):

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

Mario Carneiro (May 14 2020 at 02:11):

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

Nam (May 14 2020 at 02:16):

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 (May 14 2020 at 02:17):

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

Mario Carneiro (May 14 2020 at 02:30):

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 (May 14 2020 at 02:31):

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 (May 14 2020 at 02:35):

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 (May 14 2020 at 02:36):

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

Mario Carneiro (May 14 2020 at 02:38):

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 (May 14 2020 at 03:48):

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 (May 14 2020 at 04:42):

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 (May 14 2020 at 16:43):

"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 (May 14 2020 at 16:52):

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

Johan Commelin (May 14 2020 at 16:53):

That's a very brief summary.

Johan Commelin (May 14 2020 at 16:53):

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

Patrick Massot (May 14 2020 at 17:09):

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

Mario Carneiro (May 14 2020 at 17:14):

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

Reid Barton (May 14 2020 at 17:15):

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

Mario Carneiro (May 14 2020 at 17:15):

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

Reid Barton (May 14 2020 at 17:15):

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

Mario Carneiro (May 14 2020 at 17:17):

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 (May 14 2020 at 17:17):

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

Mario Carneiro (May 14 2020 at 17:19):

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 (May 14 2020 at 17:20):

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

Anne Baanen (May 15 2020 at 09:30):

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 (May 15 2020 at 13:58):

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


Last updated: Dec 20 2023 at 11:08 UTC