Ein Scala Type Beispiel nach Haskell

Ich habe ein wirklich interessantes Beispiel in einem Scala Artikel gefunden und frage mich, wie es in Haskell kodiert sein könnte.Ein Scala Type Beispiel nach Haskell

trait Status 
trait Open extends Status 
trait Closed extends Status 

trait Door[S <: Status] 
object Door { 
    def apply[S <: Status] = new Door[S] {} 

    def open[S <: Closed](d: Door[S]) = Door[Open] 
    def close[S <: Open](d: Door[S]) = Door[Closed] 
} 

val closedDoor = Door[Closed] 
val openDoor = Door.open(closedDoor) 
val closedAgainDoor = Door.close(openDoor) 

//val closedClosedDoor = Door.close(closedDoor) // fails to compile 
//val openOpenDoor = Door.open(openDoor) // fails to compile

Diese Probe kodiert auf der Typebene, die Sie nur eine geschlossene Door öffnen kann, und nur ein offenes Door schließen. Mein erster Versuch wurde mit nur einfache Datentypen, aber nicht wie beabsichtigt:

data Status = Open | Closed deriving (Show) 
data Door = Door Status deriving (Show) 

open :: Door -> Door 
open (Door Closed) = Door Open 

close :: Door -> Door 
close (Door Open) = Door Closed 

main = do 
    let closedDoor = (Door Closed) 
    let openDoor = open closedDoor 
    let closedAgainDoor = close openDoor 
    let closeClosedDoor = close closedDoor 
    let openOpenedDoor = open openDoor 
    print closedAgainDoor

Dies kompiliert tatsächlich (es sei denn, ich versuche closeClosedDoor oder openOpenedDoor zu drucken, die dann beschwert sich über nicht erschöpfende Muster in Funktion offen, das ist offensichtlich)

Also ich versuche herauszufinden, ob GADTs unsere Type Families diese Aufgabe erfüllen können, aber ich bin noch nicht in der Lage zu verstehen, wie es geht.

Irgendwelche Ideen?

Quelle

2016-12-02 Nigel Benns

Neben bheklilr Antwort, könnten Sie einige Typ Erweiterungen verwenden noch näher an der Scala Beispiel zu bekommen und ausschließen Nicht-sensical Typen wie

Door String

Mit DataKinds, könnten Sie die Phantom-Typ effektiv nicht zulassen aus alles andere als ein Status.

{-# LANGUAGE DataKinds #-} 

data Door (status :: Status) = Door 
data Status = Open | Closed 

open :: Door Closed -> Door Open 
open _ = Door 

close :: Door Open -> Door Closed 
close _ = Door

Dann mit Typ-Familien konnten wir auch definieren, was es heißt, „Toggle“ eine Tür

{-# LANGUAGE TypeFamilies #-} 

type family Toggle (s :: Status) where 
    Toggle Open = Closed 
    Toggle Closed = Open 

toggle :: Door s -> Door (Toggle s) 
toggle Door = Door

als Schließ gedacht, kann es schöner sein, eine GADT zu verwenden für Door - nur damit Sie zwei verschiedene Konstruktornamen haben. Ich persönlich denke, das liest sich besser

{-# LANGUAGE GADTs, DataKinds, TypeFamilies #-} 

data Door (status :: Status) where 
    OpenDoor :: Door Open 
    ClosedDoor :: Door Closed 

open :: Door Closed -> Door Open 
open _ = OpenDoor 

close :: Door Open -> Door Closed 
close _ = ClosedDoor 

toggle :: Door s -> Door (Toggle s) 
toggle OpenDoor = ClosedDoor 
toggle ClosedDoor = OpenDoor

Quelle

2016-12-02 19:37:37 Alec

Sie schlagen mich auf die 'DataKinds' Antwort. Ich wollte es nicht posten, ohne es zuerst kompiliert zu haben, aber ich musste zuerst 'stack setup' ausführen, und das dauert eine Weile in einem langsamen Netzwerk, lol. Ich mag die 'toggle' Idee mit' TypeFamilies', hatte aber nicht daran gedacht. – bheklilr

Schön, ich glaube nicht, dass ich selbst dazu gekommen wäre, immer noch die fortgeschrittenen Merkmale der Sprache zu lernen. –

Für eine bessere Schlussfolgerung, 'toggle :: (s ~ Umschalt t, t ~ Toggle s) => Tür s -> Tür t'. Oder 'Klasse Toggled s t | s -> t, t -> s wo toggle :: Tür s -> Tür t'. Du könntest wahrscheinlich eine injektive Art für GHC 8 verwenden, aber ich kaufe diese noch nicht. – dfeuer

würde ich so etwas wie

data Open = Open deriving (Show) 
data Closed = Closed deriving (Show) 
data Door door_state = Door deriving (Show) 

open :: Door Closed -> Door Open 
open _ = Door 

close :: Door Open -> Door Closed 
close _ = Door

tut Jetzt gibt es keine Fälle zu betrachten, der Staat selbst kodiert wird, in der Art, wie es mit dem Scala Beispiel.

Quelle

2016-12-02 19:25:28 bheklilr

Ein Scala Type Beispiel nach Haskell

Antwort

Verwandte Themen