Good question, damfino a formal definition off the top of my head. Except maybe "things that make up Scott encodings", but that's circular. If we're talking about plain algebraic types, either : (A -> C) -> (B -> C) -> A + B -> C and uncurry : (A -> B -> C) -> A x B -> C are eliminators for sum and product types, and K-combinator is an eliminator for both void and unit types. But as zeit_raffer hints below, those can be extended even to dependent types, let alone GADTs, but I'm not prepared to give a formal definition. He probably could, he was working on dependent sum/product eliminators in various encodings recently.
I never heard of it, but I liked this Quora answer about eliminator: https://www.quora.com/In-type-theory-what-is-an-eliminator-and-what-is-its-opposite
"An eliminator for a type is an operator or construct which characterises the use of the type's inhabitants. For example, application is an eliminator for function types; projections are eliminators for record types; conditional expression is an eliminator for Booleans."
I'm pretty much familiar with the logical aspect; did not know it's applicable to types. I mean, Kripke semantics of course allows this interpretation.
I see. Yeah, if you read MLTT or HoTT, they introduce the rules as introductions and eliminations - to the extent that foldr is a called a List eliminator.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2016-12-19 09:04 am (UTC)no subject
Date: 2016-12-19 04:52 pm (UTC)no subject
Date: 2016-12-19 06:03 pm (UTC)either : (A -> C) -> (B -> C) -> A + B -> Canduncurry : (A -> B -> C) -> A x B -> Care eliminators for sum and product types, and K-combinator is an eliminator for both void and unit types. But asno subject
Date: 2016-12-19 08:02 pm (UTC)"An eliminator for a type is an operator or construct which characterises the use of the type's inhabitants. For example, application is an eliminator for function types; projections are eliminators for record types; conditional expression is an eliminator for Booleans."
no subject
Date: 2016-12-19 08:47 pm (UTC)no subject
Date: 2016-12-20 12:42 am (UTC)no subject
Date: 2016-12-20 03:58 am (UTC)no subject
Date: 2016-12-20 07:41 am (UTC)no subject
Date: 2016-12-20 08:34 am (UTC)no subject
Date: 2016-12-19 10:17 am (UTC)Тихон в примечании сомневается в элиминаторах для Gadt. Фома неверующий.