Kind Demotion (w przeciwieństwie do promocji Kind)

Rozszerzenie DataKinds promuje "wartości" (tj. Konstruktorów) w typy. Na przykład True i False stają się odrębnymi rodzajami rodzaju Bool.Kind Demotion (w przeciwieństwie do promocji Kind)

Co chciałbym zrobić, to odwrotnie, tzn. Zdegradować typy do wartości. Funkcja z tego podpisu będzie dobrze:

demote :: Proxy (a :: t) -> t

I może faktycznie to zrobić, na przykład dla Bool:

class DemoteBool (a :: Bool) where 
    demoteBool :: Proxy (a :: Bool) -> Bool 

instance DemoteBool True where 
    demoteBool _ = True 

instance DemoteBool False where 
    demoteBool _ = False

jednak musiałbym napisać instancje dla każdego typu chcę zdegradować z powrotem do jego wartości. Czy jest lepszy sposób na zrobienie tego, który nie wymaga tak wiele bojownicy?

Źródło

2016-11-21 Clinton

Powodem, dla którego musisz to zrobić ręcznie, jest stronniczość. Biorąc pod uwagę typ 'b :: Bool', nie wiesz na pewno, że jest to' True' lub 'False'. Może to być typ zablokowany (https://typesandkinds.wordpress.com/2015/09/09/what-are-type-families/). Singleton udowadnia, że jego typ nie utknął. Zależny Haskell pomoże nieco w tym konkretnym przypadku, ponieważ "Prawda" i "Prawda" będą identyczne, ale nadal istnieją nieuniknione problemy z stronniczością. –

@BenjaminHodgson czy w ogóle istnieje tutaj pomoc "TypeInType', czy to nie ma związku? – porges

Byłoby fajnie, gdyby surowe pola po podniesieniu nie mogły zawierać zablokowanych typów, tak jak ścisłe pole nie może zawierać dna. Po prostu chcę móc przeskakiwać 'a ::! Bool' i używać go w kodzie :) – porges

To jedno z zastosowań singletons, w szczególności fromSing:

ghci> :m +Data.Singletons.Prelude 
ghci> :set -XDataKinds 
ghci> fromSing (sing :: Sing 'True) 
True

To wciąż wymaga dużo boilerplate, ale pakiet ma wiele z nich już zdefiniowane i wierzę, że zapewnia Template Haskell do pozwala łatwiej generować własne (i mniej kodu).

Źródło

2016-11-21 23:38:53

Kind Demotion (w przeciwieństwie do promocji Kind)

Odpowiedz

Powiązane problemy