Phantomtypen definieren - Beispiele können nicht kompiliert werden

Question

Ich versuche, mehr über Phantomtypen zu erfahren. Ich versuche Fun with Phantom Types von Ralf Hinze zu lesen. Er benutzt ein Schlüsselwort with, das ich vorher nicht gesehen habe und das ich nicht kompilieren kann. Ich bekomme einen Parse-Fehler auf =, wenn ich dies versuche.

data Type t = RInt     with t = Int 
      | RChar     with t = Char 
      | RList (Type a)   with t = [a ] 
      | RPair (Type a) (Type b) with t = (a, b) 

Früher in dem Papier, sagt er, dass die „mit“ Aussagen nicht unbedingt erforderlich sind, dass Sie a = t stattdessen setzen können, aber ich kann nicht herausfinden, wie dieser Datentyp ohne sie zu definieren. Die folgenden Fehler mit: Not in scope: type variable 'a'

data Type t = RInt 
      | RChar 
      | RList (Type a) 
      | RPair (Type a) (Type b) 

Was fehlt mir?

Answer 1

Meine Vermutung ist, dass die Definition Sans-with in dem Papier vorgeschlagen ist

data Type t = RInt 
      | RChar 
      | RList (Type t) 
      | RPair (Type t) (Type t) 

Oberhalb der Parameter t wird nie verwendet. Es ist tatsächlich Phantom.

Dies bedeutet, dass z.B.

RInt :: Type a 

für jeden Typen a. Im Gegensatz dazu, wenn die with Einschränkungen eingehalten würden, wäre es unmöglich, RInt :: Type t für jede t außer für t ~ Int zu haben.

Die with Syntax ist nicht in GHC vorhanden, aber GADTs spielen im Wesentlichen die gleiche Rolle.

{-# LANGUAGE GADTs #-} 
data Type t where 
    RInt :: t ~ Int => Type t 
    RChar :: t ~ Char => Type t 
    RList :: t ~ [a] => Type a -> Type t 
    RPair :: t ~ (a,b) => Type a -> Type b -> Type t 

Beachten Sie, wie with durch eine Gleichheit Einschränkung in jedem Konstruktor ersetzt wird. Es ist im Grunde dasselbe, anders geschrieben.

kompakter, können wir die oben in

data Type t where 
    RInt :: Type Int 
    RChar :: Type Char 
    RList :: Type a -> Type [a] 
    RPair :: Type a -> Type b -> Type (a,b) 

umschreiben, wo die Einschränkungen wurden in der letzten Art „inlined“.

Answer 2

Obwohl hässlich, wird das Folgende funktionieren und könnte etwas näher an dieser Notation im Geiste betrachtet werden. Dies entzieht einem GADT im Wesentlichen Typgleichheiten (die scheinbar keine eigene Erweiterung haben, so dass Sie entweder aktivieren müssen, um sie zu verwenden) und Existenzen.

{-# LANGUAGE ExistentialQuantification, TypeFamilies #-} 

data Type t = t ~ Int => RInt 
      | t ~ Char => RChar 
      | forall a. t ~ [a] => RList (Type a) 
      | forall a b. t ~ (a, b) => RPair (Type a) (Type b)