/ / Prečo sa mi nezhoduje s typom rodiny? - haskell, typy

Prečo nemôžem porovnať vzor na rodine typu? - haskell, typy

Zvážte nasledujúci kód:

{-# LANGUAGE TypeFamilies #-}

data Twothings a b = Twothings a b

type family Leftthing a where
Leftthing (Twothings a b) = Leftthing a
Leftthing a = a

leftthing :: a -> Leftthing a
leftthing (Twothings a b) = leftthing a
leftthing b = b

Nevytvára sa s nasledujúcou chybou:

Couldn"t match expected type ‘a’
with actual type ‘Twothings a0 t0’
‘a’ is a rigid type variable bound by
the type signature for:
leftthing :: forall a. a -> Leftthing a

Sťažuje sa na linku leftthing (Twothings a b) = leftthing a, Ak správne chápem, nemôže to zjednotiť typovú premennú a v typovom podpisu s typom konštruktora Twothings, Ok, zdá sa, že to má zmysel. Ale potom, ako môžem niekedy definovať funkciu so skupinami typov v typovom podpisu?

odpovede:

11 pre odpoveď č. 1

Keď vyhlasujete

leftthing :: a -> Leftthing a

hovoríte, že návštevník z leftthing sa rozhodne, čo a je.

Keď píšete

leftthing (Twothings a b) = leftthing a

ty si za predpokladu, že si vybrali Twothings typ, a to nie je nevyhnutne prípad, váš program je zamietnutý.

Možno ste si mysleli, že ste boli testovanie, či zvolili si Twothings typ, ale nie! Informácie o type sú vymazané pred časom spustenia, takže neexistuje spôsob, ako vykonať takýto test.

vy môcť pokúste sa obnoviť potrebné informácie o čase spustenia. Najskôr mi dovoľte opraviť rozpor medzi vašou Leftthing a leftthing.

type family Leftthing a where
Leftthing (Twothings a b) = Leftthing{-you forgot the recursion!-} a
Leftthing a = a

Teraz môžeme definovať GADT svedkov Twothingvýbežok.

data IsItTwothings :: * -> * where
YesItIs   :: IsItTwothings a -> IsItTwothings (Twothings a b)
NoItIsn"t :: Leftthing a ~ a => IsItTwothings a
-- ^^^^^^^^^^^^^^^ this constraint will hold for any type
-- which is *definitely not* a Twothings type

A potom môžeme prejsť svedok ako argument:

leftthing :: IsItTwothings a -> a -> Leftthing a
leftthing (YesItIs r) (Twothings a b) = leftthing r a
leftthing NoItIsn"t   b               = b

V skutočnosti je svedkom unary kódovanie počtu ľavicovo vnorených Twothingses u koreňa vášho typu. To je dostatok informácií, aby ste v čase spustenia určili správne množstvo rozbaľovania.

> leftthing (YesItIs (YesItIs NoItIsn"t)) (Twothings (Twothings True 11) (Twothings "strange" [42]))
True

Ak chcete zhrnúť, nemôžete zistiť typ podľa vzoruzhody na hodnote. Musíte skôr vedieť, aký typ chcete urobiť (pretože typ určuje rozloženie pamäte a nie sú tam žiadne tagy typu run time). Nemôžete vzorovú zhodu na typoch priamo (pretože nie sú tam, na ktoré sa majú zhodovať). Môžete vytvoriť typy údajov, ktoré fungujú ako dôkaz o čase spustenia typu štruktúry a zhodujú sa na nich.

Možno, jeden deň, váš program bude fungovať, ak mu to dáte

leftthing :: pi a. a -> Leftthing a

kde pi je závislý kvantifikátor, čo naznačuje, že argument skrytého typu nie je vymazaný, ale skôr prešiel a spárovaný v čase spustenia. Ten deň ešte nenastal, ale myslím, že to bude.