Zulip Chat Archive

Stream: new members

Topic: Reducing functions that return types


view this post on Zulip Kevin Sullivan (Oct 18 2020 at 18:17):

YEP below works. NOPE doesn't. Where exactly does the latter fail? Beginner question.

inductive foo : Type
| R
| N

def typeForFoo : foo  Type
| foo.R := 
| foo.N := 

-- YEP!
def r : (typeForFoo foo.R) := (1.0 : )
def n : (typeForFoo foo.N) := (1 : )

structure bar := mk :: (r : ) (n : )

-- NOPE!
def jack (f : foo) (s : typeForFoo f) : bar :=
match f with
| foo.R := bar.mk s 0
| foo.N := bar.mk 0 s
end

view this post on Zulip Kevin Sullivan (Oct 18 2020 at 18:19):

Involves matching on a type, which is inconsistent?

view this post on Zulip Mario Carneiro (Oct 18 2020 at 18:20):

well for starters #eval doesn't work on real numbers

view this post on Zulip Mario Carneiro (Oct 18 2020 at 18:20):

also you are missing your prologue for the #mwe

view this post on Zulip Kevin Sullivan (Oct 18 2020 at 18:21):

The problem is in jack. Each of the s is read as being of type (typeForFoo f) not as the reduced value of that expression. Yes, ok, on the evals (deleted), and sorry about missing import of reals from mathlib.

view this post on Zulip Mario Carneiro (Oct 18 2020 at 18:24):

Because s depends on f, you have to match on them together

def jack (f : foo) (s : typeForFoo f) : bar :=
match f, s with
| foo.R, s := bar.mk s 0
| foo.N, s := bar.mk 0 s
end

view this post on Zulip Kevin Sullivan (Oct 18 2020 at 18:33):

Thank you, Mario.

Mario Carneiro said:

Because s depends on f, you have to match on them together

def jack (f : foo) (s : typeForFoo f) : bar :=
match f, s with
| foo.R, s := bar.mk s 0
| foo.N, s := bar.mk 0 s
end

Last updated: May 10 2021 at 18:22 UTC