Zulip Chat Archive

Stream: new members

Topic: Reducing functions that return types


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

Kevin Sullivan (Oct 18 2020 at 18:19):

Involves matching on a type, which is inconsistent?

Mario Carneiro (Oct 18 2020 at 18:20):

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

Mario Carneiro (Oct 18 2020 at 18:20):

also you are missing your prologue for the #mwe

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.

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

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: Dec 20 2023 at 11:08 UTC