Limitazione dei tipi di dati

Question

Supponiamo di avere una buona definizione induttiva e di definirla come un tipo di dati in Haskell. Tuttavia, la tua definizione induttiva è (come molte definizioni induttive sono) di una tale forma che le regole generatrici richiedono che le loro "premesse" abbiano una certa struttura. Per esempio, supponiamo di avere la seguente definizione:

• se x è un intero pari, poi T x è un'arma,
• se x è un intero dispari, quindi S x è un'arma.

Se voglio definire questo (come un unico) tipo di dati in Haskell, vorrei scrivere qualcosa di simile

data Weapon = T Int | S Int 

Ovviamente, questo non funzionerà come è ora possibile generare T 5 e S 4, per esempio. Esiste un modo naturale per passare delle restrizioni sugli argomenti del costruttore, in modo che io possa scrivere qualcosa di simile al codice precedente che darebbe la definizione corretta?

Answer 1

Il tuo colpo migliore è di non esportare T e S esplicitamente, ma consentono un costruttore personalizzato:

module YourModule (Weapon, smartConstruct) where 

data Weapon = T Int | S Int 

smartConstruct :: Int -> Weapon 
smartConstruct x 
    | even x  = T x 
    | otherwise = S x 

Ora, quando l'importazione YourModule, gli utenti non saranno in grado di creare e TS esplicitamente, ma solo con la tua funzione smartConstruct.

Answer 2

Questo è un po 'non-Haskelly, ma è più idiomatico in es. Agda: cambia l'interpretazione della tua rappresentazione in modo che sia costretta a essere corretta per costruzione.

In questo caso, notare che se n :: Int, quindi even (2 * n) e odd (2 * n + 1). Se allontaniamo il caso di troppo grandi Int s, possiamo dire che c'è una biiezione tra lo Int s e lo Int s; e un altro tra il dispari Int s e il Int s.

Così, attraverso questo, si può scegliere questa rappresentazione:

data Weapon = T Int | S Int 

e cambiare la sua interpretazione in modo tale che il valore T n in realtà rappresenta T (2 * n) e il valore S n rappresenta S (2 * n + 1). Pertanto, a prescindere da quale sia il codice n :: Int che scegli, il codice T n sarà valido poiché lo considererai come il valore "T -of-2 * n".

Answer 3

Se si è disposti a limitare l'utilizzo di Nats e se si utilizza la magia di tipo ragionevolmente avanzato, è possibile utilizzare GHC.TypeLits.

{-# LANGUAGE DataKinds, GADTs, TypeOperators, KindSignatures #-} 

import GHC.TypeLits 

data Weapon (n :: Nat) where 
    Banana  :: n ~ (2 * m) => Weapon n 
    PointyStick :: n ~ (2 * m + 1) => Weapon n 

banana :: Weapon 2 
banana = Banana 

pointyStick :: Weapon 3 
pointyStick = PointyStick 

provare per lei, che non si compila con (anche dispari /) numeri sbagliati.

Modifica: Più pratico è probabilmente l'approccio di cactus però.