Constructor, die (über DataKinds) hebt an * -> A

Question

ein ADT wie

data K = A | B Bool 

Given die DataKinds Erweiterung uns es in Arten und Typen/Typkonstruktoren

K :: BOX 
'A :: K 
'B :: 'Bool -> K 

Gibt es zu heben erlaubt ein Weg, um einen Konstruktor K, die den Typkonstruktor

'C :: * -> K 

hebt hinzufügen?

Answer 1

Wie Conor erklärt, ist dies nicht direkt möglich. Sie können jedoch definieren

data K a = ... | C a 

Dann ist diese zu

C :: a -> K a 

fördert Wenn Sie dann K * verwenden, können Sie erreichen, was Sie wollen.

Answer 2

Im Moment habe ich keine Angst. Ich habe auch keine offensichtliche Problemumgehung entdeckt.

This ticket dokumentiert die Aussichten für die Deklaration von Datenarten, geborene Art, anstatt Datentypen mit Freundlichkeit Schub auf ihnen. Es wäre völlig vernünftig für die Konstrukteure solcher Dinge, Typen zu verpacken, wie Sie es vorschlagen. Wir sind noch nicht dort, aber es sieht nicht so problematisch aus.

Meine Augen sind auf einem größeren Preis. Ich möchte * eine durchaus sinnvolle Art von Laufzeitwerten sein, damit die Art, die du willst, durch Werbung so existieren kann, wie wir sie heute haben. Kombinieren Sie das mit dem Begriff des pi-Typs (nichtparametrische Abstraktion über den Teil der Sprache, der effektiv von Typen und Werten geteilt wird), und wir könnten einen direkteren Weg finden, Ad-hoc-Abstraktionen zu machen als mit Data.Typeable. Das übliche forall würde parametrisch bleiben.