Czy mam na myśli i używam typów singleton w Haskell?

Question

Chcę utworzyć kilka niezgodnych, ale poza tym równe, typy danych. Oznacza to, że chciałbym mieć sparametryzowanego typu Foo a, a funkcje takie jak

bar :: (Foo a) -> (Foo a) -> (Foo a) 

bez faktycznie dbając o co a jest. Aby wyjaśnić dalej, chciałbym system typu powstrzymać mnie od robienia

x :: Foo Int 
y :: Foo Char 
bar x y 

podczas gdy w tym samym czasie nie troszczą się o Int i Char (I tylko obchodzi, że nie są one takie same) .

W moim rzeczywistym kodzie mam typ wielomianów nad danym pierścieniem. Właściwie to nie obchodzi mnie to, co nieokreślone, o ile system typów powstrzymuje mnie od dodania wielomianu wt z wielomianem w s. Jak dotąd rozwiązać to poprzez stworzenie typeclass Indeterminate i parametryzacji mój typ wielomianu jako

data (Ring a, Indeterminate b) => Polynomial a b 

To podejście czuje się zupełnie naturalne dla Ring części dlatego zrobić dbają o których szczególności pierścień dany wielomian jest skończona . Wydaje się to bardzo wymyślne dla części Indeterminate, jak opisano poniżej.

Powyższe podejście działa dobrze, ale jest wyrafinowane. Zwłaszcza więc ta część:

class Indeterminate a where 
    indeterminate :: a 

data T = T 

instance Indeterminate T where 
    indeterminate = T 

data S = S 

instance Indeterminate S where 
    indeterminate = S 

(i tak dalej może być jeszcze kilka nieokreślonych). Czuje się dziwnie i źle. Zasadniczo staram się wymagać, aby instancje Indeterminate były singletons (w this sense). Uczucie dziwności jest jednym ze wskaźników, że mogę atakować to niesłusznie. Innym jest fakt, że w końcu muszę opisywać wiele z moich Polynomial a b s, ponieważ rzeczywisty typ b często nie może być wywnioskowany (to nie jest dziwne, ale jest denerwujące).

Wszelkie sugestie? Czy powinienem dalej robić to w ten sposób, czy też czegoś brakuje?

PS: Nie obrażaj się, jeśli nie zareaguję natychmiastowo i nie przyjmuję odpowiedzi. Nie będę mógł wrócić z powrotem przez kilka dni.

Answer 1

Przede wszystkim, nie jestem pewien, że to:

data (Ring a, Indeterminate b) => Polynomial a b 

... robi to, czego oczekują go. Konteksty na data definicji nie są zbyt użyteczne - patrz the discussion here kilku powodów, z których kwota do nich najbardziej zmuszając dodać dodatkowe adnotacje bez faktycznie zapewniając wiele dodatkowych gwarancji typu.

Po drugie, czy rzeczywiście zależy ci na parametrze "nieokreślonym", niż na upewnieniu się, że typy są różne? Dosyć normalnym sposobem robienia tego typu rzeczy jest to, co nazywane jest phantom types - z założenia parametrami w konstruktorze typów, które nie są używane w konstruktorze danych. Nigdy nie używaj ani nie potrzebują wartość typu phantom, więc funkcje mogą być polimorficzne, jak chcesz, np:

data Foo a b = Foo b 

foo :: Foo a b -> Foo a b 
foo (Foo x) = Foo x 

bar :: Foo a c -> Foo b c 
bar (Foo x) = Foo x 

baz :: Foo Int Int -> Foo Char Int -> Foo() Int 
baz (Foo x) (Foo y) = Foo $ x + y 

Oczywiście to wymaga adnotacji, ale tylko w miejscach, gdzie jesteś celowo dodanie ograniczeń .W przeciwnym razie, wnioskowanie będzie działać normalnie dla parametru typu fantomowego.

Wydaje mi się, że powyższe podejście powinno wystarczyć do tego, co tu robisz - biznes z typami singleton polega głównie na wypełnianiu luki między bardziej skomplikowanymi elementami na poziomie typu a regularnymi obliczeniami wartości na podstawie tworzenia wpisz proxy dla wartości. Może to być przydatne, na przykład, do oznaczania wektorów typami, które wskazują ich podstawę, lub oznaczaniem wartości numerycznych jednostkami fizycznymi - w obu przypadkach adnotacja ma większe znaczenie niż tylko "nieokreślona nazwa X".