Zulip Chat Archive

Stream: new members

Topic: hitchhiker's guide


view this post on Zulip Nam (May 06 2020 at 21:37):

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

view this post on Zulip 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])

view this post on Zulip Kevin Buzzard (May 06 2020 at 21:37):

[] has even length

view this post on Zulip Nam (May 06 2020 at 21:38):

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

view this post on Zulip Nam (May 06 2020 at 21:39):

i read it wrongly to be two lists sandwiching an element

view this post on Zulip Jasmin Blanchette (May 07 2020 at 05:18):

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

view this post on Zulip Kevin Buzzard (May 07 2020 at 09:28):

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

view this post on Zulip Kevin Buzzard (May 07 2020 at 09:28):

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

view this post on Zulip 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".

view this post on Zulip Aniruddh Agarwal (May 08 2020 at 15:43):

Thereby allowing division by 0? :grinning_face_with_smiling_eyes:

view this post on Zulip Reid Barton (May 08 2020 at 16:08):

Division by what now?

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 11 2020 at 01:49):

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

view this post on Zulip Mario Carneiro (May 11 2020 at 01:49):

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

view this post on Zulip 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)

view this post on Zulip Nam (May 11 2020 at 02:21):

so the first def is like a typedef in C?

view this post on Zulip Nam (May 11 2020 at 02:21):

is there a keyword for that? say, alias?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip Nam (May 14 2020 at 02:08):

i see. thank you!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Nam (May 14 2020 at 02:17):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 14 2020 at 16:52):

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

view this post on Zulip Johan Commelin (May 14 2020 at 16:53):

That's a very brief summary.

view this post on Zulip 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".

view this post on Zulip Patrick Massot (May 14 2020 at 17:09):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (May 14 2020 at 17:15):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (May 14 2020 at 17:15):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 14 2020 at 17:17):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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: May 10 2021 at 00:31 UTC