هم‌وردایی و پادوردایی (علوم رایانه)
سیستم گونه سازی در بسیاری از زبانهای برنامه‌نویسی زیرگونه سازی را پشتیبانی می‌کند. برای نمونه، اگر کلاس A زیرگونه‌ای از کلاس B باشد، عبارتی از گونه A می‌تواند هرجاییکه یک عبارت از گونه B وجود داشته باشد، بکار رود. هم‌وردایی به ارتباط زیرگونه سازی در گونه‌های پیچیده (لیستی از Aها در برابر لیستی از Bها، متودی که A را برمی‌گرداند در برابر متودی که B را برمی‌گرداند، و …) و مؤلفه‌های آن‌ها گفته می‌شود. بسته به وردایی type constructor، رابطه زیرگونه سازی ممکن است حفظ شود، برعکس شود یا نادیده گرفته شود. برای نمونه در اکمل «لیستی از Aها» زیرگونه از «لیستی از Bها» است چراکه constructor لیست هم‌وردا است، درحالیکه متودی با وردودی B و خروجی String زیرگونه‌ای از متودی با ورودی A و خروجی String است چراکه Function type constructor پادوردا در نوع پارامترهاست.
طراح زبان برنامه‌نویسی مسئله وردایی را در طراحی گونه سازی در آرایه‌ها، وارثت، و انواع داده generic در نظر می‌گیرد. با بکارگیری type constructorهای هم‌وردا و پادوردا به جای ناوردا، بیشتر برنامه‌ها به عنوان برنامه‌های well-typed پذیرفته می‌شوند. از سویی دیگر، اکثر برنامه نویسان پادوردایی را غیرشهودی می‌یابند و ردیابی دقیق وردایی برای اجتناب از خطاهای زمان اجرا، منجر به قواعد گونه سازی پیچیده می‌شود. به منظور ساده‌سازی سیستم گونه سازی، یک زبان برنامه‌نویسی ممکن است type constructor را به صورت ناوردا در نظر بگیرد حتی اگر وردا در نظر گرفتن آن خطری نداشته باشد یا به صورت هم‌وردا در نظر بگیرد حتی اگر type safety زیر سؤال برود.
فرهنگستان زبان فارسی، وردیدن از ریشه باستانی ورت (ورتیدن)، را بجای فعل to vary برگزیده است و از این فعل مشتقات وردایی(variance)،وردش(variation)، وردا(variant)، هم‌وردا(covariant)، هم وردایی(covariance)، ناوردا(invariant)، ناوردایی(invariance)، پادوردا(contravariance) را برساخته است.
در سیستم گونه سازی یک زبان برنامه‌نویسی روش گونه سازی یا type constructor
برای نمونه در سی شارپ:
وقتی یک کلاس فرزند یک متود از یک کلاس پدر را Override می‌کند، کامپایلر باید درستی نوع متود را چک کند. در برخی از زبان‌ها نوع باید دقیقاً منطبق بر نوع کلاس پدر باشد (ناوردایی). بر اساس روش زیرگونه سازی معمول برای function typeها، متود override شده می‌تواند نوع خاص تری را برگرداند (هم وردایی) و نوع عام تری را به عنوان آرگومان ورودی بپذیرد (پادوردایی نوع آرگومان). در نمادگان UML، حالت‌های ممکن عبارتند از
برای داشتن نمونه‌های ملموس، فرض کنید کلاسی داریم برای مدل کردن یک پناهگاه جانوران. همچنین کلاس Cat زیرگونه ای از کلاس Animal است.
پرسش: اگر از کلاس AnimalShelter یک زیرگونه بسازیم چه انواعی برای getAnimalForAdoption و putAnimal پذیرفته می‌شوند؟
در زبانی که مقدار بازگشتی هم‌وردا را پشتیبانی می‌کند، کلاس مشتق شده می‌تواند متود getAnimalForAdoption را override کند و متود override شده نوع خاص تری را بازگرداند:
در میان زبان‌های شی گرا، Java و C++ نوع مقدار بازگشتی هم‌وردا را پشتیبانی می‌کنند در حالیکه C# پشتیبانی نمی‌کند. افزودن نوع مقدار بازگشتی هم‌وردا یکی از نخستین اصلاحات زبان C++ بود که توسط کمیته استاندارد در سال ۱۹۹۸ تأیید شد.
Scala و D نیز نوع مقدار بازگشتی هم‌وردا را پشتیبانی می‌کنند.
در زبان Eiffel یک متود override شده می‌تواند نوع خاص تری از نوع آرگومان متود کلاس پدر خود بپذیرد (هم‌وردایی در نوع آرگومان). بنابراین، کد زیر را ببینید:
این type safe نیست. چرا که با تبدیل CatShelter به AnimalShelter (به اصلاح up-casting)، می‌توان هنگام نوشتن برنامه، یک سگ را در پناهگاه گربه‌ها قرار داد که با توجه به تجاوز از محدودیت‌های آرگومان CatShelter، در زمان اجرا خطا می‌دهد. نبود Type safety (که به عنوان "catcall problem" در جامعه Eiffel نیز شناخته می‌شود) به عنوان مشکل اساسی مطرح است.
جدول زیر روش‌های overriding متودها در برخی از زبان‌های برنامه‌نویسی را نشان می‌دهد.
این اصطلاحات از مفهوم عملگر در نظریه رده‌ها آمده‌است. رده formula_1 را در نظر بگیرید که اشیاع آن نوع‌ها هستند و ریختارهای آن روابط زیرگونه‌ها را نشان می‌دهند ≤. برای نمونه یک function type constructor دو نوع "p" و "r" را می‌گیرد و نوع جدید "p" → "r" را ایجاد می‌کند؛ بنابراین اشیایی در formula_2 را به اشیایی در formula_1 می‌برد. بر اساس روش زیرگونه سازی برای function typeها این عملیات ≤ را برای آرگومان نخست برعکس می‌کند و برای برای آرگومان دوم حفظ می‌کند؛ بنابراین این عملگر در آرگومان نخست پادوردا و در آرگومان دوم همورداست.