Fórum Root.cz
Hlavní témata => Vývoj => Téma založeno: Russell 06. 03. 2018, 10:20:33
-
Poslední dobou tu je nějak natrolleno, tak snad vážně míněný dotaz nezapadne. Máte někdo nějaký názorný příklad identitních typů v homotopické teorii typů? V teorii typů chápu všechno až po závislostní typy (které teď pozvolna pronikají do Haskellu), ale u identit mě nenapadá žádná instance kromě triviálního (extenziálního) porovnání. Přitom homotopií by měla být hromada. Uvítám také typy na jazyky, ve kterých se dá s identitami pracovat, ovšem primárně mi jde o příklad bez ohledu na jazyk.
-
názorný příklad identitních typů v homotopické teorii typů?
Jak na to tak koukám, tak s "normální" (tj. matematickou) homotopií to moc společného nemá, až na hierarchii.
-
Poslední dobou tu je nějak natrolleno, tak snad vážně míněný dotaz nezapadne. Máte někdo nějaký názorný příklad identitních typů v homotopické teorii typů? V teorii typů chápu všechno až po závislostní typy (které teď pozvolna pronikají do Haskellu), ale u identit mě nenapadá žádná instance kromě triviálního (extenziálního) porovnání. Přitom homotopií by měla být hromada. Uvítám také typy na jazyky, ve kterých se dá s identitami pracovat, ovšem primárně mi jde o příklad bez ohledu na jazyk.
Id typy se v programování nepoužívají, protože mají v příčetných typových systémech nanejvýš jeden prvek, čímž tak nějak ztrácejí na atraktivitě. Netriviální příklad systému, kde mají víc členů, jsou grupoidy a isomorfismy mezi nimi. To ovšem není ani v Haskellu.