Typový system versus unittesty

[BoneFlute]

co je "typ"?

metadata k hodnote?

metadata to je neco vagniho, to muze byt treba cas vytvoreni.

Datovy typ je spis dvojice: mnozina hodnot a mnozina operaci, ne?

Množina operací asi nebude stačit. Ještě je třeba název kategorie pro nominální typování.

[Reklama]

[JSH]

co je "typ"?

metadata k hodnote?

metadata to je neco vagniho, to muze byt treba cas vytvoreni.

Datovy typ je spis dvojice: mnozina hodnot a mnozina operaci, ne?

Množina operací asi nebude stačit. Ještě je třeba název kategorie pro nominální typování.

Já bych to omezil na pojmenovanou množinu hodnot. Operace běžně pracují s více hodnotama různého typu, takže by se stejná operace dala najít ve spoustě typů.

[BoneFlute]

Datovy typ je spis dvojice: mnozina hodnot a mnozina operaci, ne?

Množina operací asi nebude stačit. Ještě je třeba název kategorie pro nominální typování.

Já bych to omezil na pojmenovanou množinu hodnot. Operace běžně pracují s více hodnotama různého typu, takže by se stejná operace dala najít ve spoustě typů.

buildPerson :: Name -> Name -> Age -> Person
bmi :: Age -> Sex -> Weight -> Height -> BMI

Samozřejmě často si vystačím jen s rozhraním na základě operací. Ale ten nominální typ mi pomůže ohlídat, že tam nervu blbost.

... ale možná že "pojmenovaná množina hodnot" je to, o čem mluvím :-) Age je pojmenovaný subset Intu. Kde potřebuju Int mohu dát Age, kde potřebuju Age nemohu dát Int.

[listoper]

Na tohle sem dnes narazil: https://serokell.io/blog/2018/12/17/why-dependent-haskell

[Bacsa]

Na tohle sem dnes narazil: https://serokell.io/blog/2018/12/17/why-dependent-haskell

Dost zajímavé, ale není to pro BFP.

[Reklama]

[Idris]

Pro rozšíření obzorů: https://www.manning.com/books/programming-with-types

[Idris]

Před pár dny jsem narazil na indexikální typy a vzpomněl si, že tebe typové systémy a intuicionistická logika zajímají, tak jen dávám tip Je to něco jako “this”, ale na úrovni typů. Jdou skrz to implementovat higher-kinded typy v systému prvního řádu (bez explicitních HKT), takže ve výsledku je takový systém formálně silnější (a kompatibilní s dědičností).

[BoneFlute]

Před pár dny jsem narazil na indexikální typy a vzpomněl si, že tebe typové systémy a intuicionistická logika zajímají, tak jen dávám tip Je to něco jako “this”, ale na úrovni typů. Jdou skrz to implementovat higher-kinded typy v systému prvního řádu (bez explicitních HKT), takže ve výsledku je takový systém formálně silnější (a kompatibilní s dědičností).

Díky. Jsem rád za každý hint.
Nějaký odkaz, článek, by nebyl?

[Idris]

Před pár dny jsem narazil na indexikální typy a vzpomněl si, že tebe typové systémy a intuicionistická logika zajímají, tak jen dávám tip Je to něco jako “this”, ale na úrovni typů. Jdou skrz to implementovat higher-kinded typy v systému prvního řádu (bez explicitních HKT), takže ve výsledku je takový systém formálně silnější (a kompatibilní s dědičností).

Díky. Jsem rád za každý hint.
Nějaký odkaz, článek, by nebyl?

Takhle z hlavy mě napadá jen dokumentace ke Swiftu, zejména použití Self a jeho spojení s asociovanými typy. Teď zrovna nemám na nic čas, ale za pár dnů k tomu můžu něco napsat tady.

[BoneFlute]

Před pár dny jsem narazil na indexikální typy a vzpomněl si, že tebe typové systémy a intuicionistická logika zajímají, tak jen dávám tip Je to něco jako “this”, ale na úrovni typů. Jdou skrz to implementovat higher-kinded typy v systému prvního řádu (bez explicitních HKT), takže ve výsledku je takový systém formálně silnější (a kompatibilní s dědičností).

Díky. Jsem rád za každý hint.
Nějaký odkaz, článek, by nebyl?

Takhle z hlavy mě napadá jen dokumentace ke Swiftu, zejména použití Self a jeho spojení s asociovanými typy. Teď zrovna nemám na nic čas, ale za pár dnů k tomu můžu něco napsat tady.

To by bylo super. Na Swift se podívám. Já hledal obecně, a našel jen něco pro TypeScript, ale to odhadem je něco jiného stejného jména.

[Idris]

To by bylo super. Na Swift se podívám. Já hledal obecně, a našel jen něco pro TypeScript, ale to odhadem je něco jiného stejného jména.

Jo, to bylo asi “indexable types”, já zmiňoval “indexical types.” To jsou typy, jejichž denotát závisí na kontextu. V podstatě něco jako “this”, ale na úrovni typů. Jsou to obecně higher-kinded typy, které žádný z hlavních OO jazyků vyjma C++ nemá. V metodách se dá používat Self[T] a podobné srandičky, což vede k mnohem silnějšímu typovému systému, než má třeba Java.

[Idris]

Zjistil jsem, že Julia má (nevím, od které verze) něco jako závislostní součtový typ (píšu “něco jako”, protože to zřejmě není zamýšlená vlastnost jejího typového systému). Dávám to sem jen jako doplňující poznámku související s tématem tohoto starého vlákna, kdyby si někdo (BoneFlute ) chtěl hrát se závislostními typy a nechce se mu otravovat s haskelloidními jazyky — Julia je přece jenom stravitelnější.

[Google CTCCTCGGCGGGCACGTAG]

Zjistil jsem, že Julia má (nevím, od které verze) něco jako závislostní součtový typ (píšu “něco jako”, protože to zřejmě není zamýšlená vlastnost jejího typového systému). Dávám to sem jen jako doplňující poznámku související s tématem tohoto starého vlákna, kdyby si někdo (BoneFlute ) chtěl hrát se závislostními typy a nechce se mu otravovat s haskelloidními jazyky — Julia je přece jenom stravitelnější.

Zavislostni typy jsou dnes mainstream

[Idris]

Zjistil jsem, že Julia má (nevím, od které verze) něco jako závislostní součtový typ (píšu “něco jako”, protože to zřejmě není zamýšlená vlastnost jejího typového systému). Dávám to sem jen jako doplňující poznámku související s tématem tohoto starého vlákna, kdyby si někdo (BoneFlute ) chtěl hrát se závislostními typy a nechce se mu otravovat s haskelloidními jazyky — Julia je přece jenom stravitelnější.

Zavislostni typy jsou dnes mainstream

 

[BoneFlute]

Zjistil jsem, že Julia má (nevím, od které verze) něco jako závislostní součtový typ (píšu “něco jako”, protože to zřejmě není zamýšlená vlastnost jejího typového systému). Dávám to sem jen jako doplňující poznámku související s tématem tohoto starého vlákna, kdyby si někdo (BoneFlute ) chtěl hrát se závislostními typy a nechce se mu otravovat s haskelloidními jazyky — Julia je přece jenom stravitelnější.

Díky.