Quali sono alcuni esempi di programmazione a livello di caratteri?

Question

Non capisco cosa significa "programmazione a livello di testo", né posso trovare una spiegazione adeguata utilizzando Google.

Qualcuno potrebbe fornire un esempio che dimostri la programmazione a livello di codice? Spiegazioni e/o definizioni del paradigma sarebbero utili e apprezzate.

Answer 1

Nella maggior parte delle lingue tipizzate staticamente si dispone di due "domini": il livello di valore e il livello di tipo (alcune lingue hanno ancora di più). La programmazione a livello di codice coinvolge la logica di codifica (spesso l'astrazione di funzioni) nel sistema di tipi che viene valutata in fase di compilazione. Alcuni esempi potrebbero essere la metaprogrammazione del modello o le famiglie di tipi Haskell.

alcune lingue estensioni sono necessari per fare questo esempio in Haskell, ma è sorta di li ignorano per ora e basta guardare il tipo di famiglia come una funzione, ma sopra i numeri tipo di livello (Nat).

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE UndecidableInstances #-} 

import GHC.TypeLits 
import Data.Proxy 

-- value-level 
odd :: Integer -> Bool 
odd 0 = False 
odd 1 = True 
odd n = odd (n-2) 

-- type-level 
type family Odd (n :: Nat) :: Bool where 
    Odd 0 = False 
    Odd 1 = True 
    Odd n = Odd (n - 2) 

test1 = Proxy :: Proxy (Odd 10) 
test2 = Proxy :: Proxy (Odd 11) 

Qui invece di testare se un numero naturale valore è un numero dispari, stiamo testando se un numero naturale tipo è un numero dispari e riducendola ad un valore booleano tipo livello al di compilazione tempo. Se si valuta questo programma i tipi di test1 e test2 sono calcolati al momento della compilazione a:

λ: :type test1 
test1 :: Proxy 'False 
λ: :type test2 
test2 :: Proxy 'True 

Questa è l'essenza della programmazione tipo di livello, a seconda della lingua si può essere in grado di codificare logica complessa al tipo - livello che ha una varietà di usi.Ad esempio, per limitare determinati comportamenti a livello di valore, gestire la finalizzazione delle risorse o memorizzare più informazioni sulle strutture dei dati.

Answer 2

Hai già familiarità con la programmazione "a livello di valore", per cui si manipolano valori come 42 :: Int o 'a' :: Char. In linguaggi come Haskell o Scala, la programmazione tipo di livello consente di manipolare tipi come Int :: * o Char :: * dove * è il tipo di tipo concreto (Maybe a o [a] sono tipi concreti, ma non Maybe o [] che hanno tipo * -> *).

Consideriamo questa funzione

foo :: Char -> Int 
foo x = fromEnum x 

Qui foo assume un valore di tipoChare restituisce un nuovo valore di tipo Int utilizzando l'istanza Enum per Char. Questa funzione manipola i valori.

Ora confrontare foo in questa famiglia di tipi, abilitata con l'estensione di lingua TypeFamilies.

type family Foo (x :: *) 
type instance Foo Char = Int 

Qui Foo prende un tipo di tipo* e restituisce un nuovo tipo di genere * utilizzando la semplice mappatura Char -> Int. Questa è una funzione di livello di tipo che manipola i tipi.

Questo è un esempio molto semplice e ci si potrebbe chiedere come questo possa essere utile. Usando strumenti di linguaggio più potenti, possiamo iniziare a codificare le prove della correttezza del nostro codice a livello di testo (per ulteriori informazioni, consultare la corrispondenza Curry-Howard).

Un esempio pratico è un albero rosso-nero che utilizza la programmazione a livello di codice per garantire staticamente la tenuta degli invarianti dell'albero.

Un albero rosso-nero ha le seguenti proprietà semplici:

1. Un nodo è rosso o nero.
2. La radice è nera.
3. Tutte le foglie sono nere. (Tutte le foglie hanno lo stesso colore della radice.)
4. Ogni nodo rosso deve avere due nodi figlio neri. Ogni percorso da un determinato nodo a una delle sue foglie discendente contiene lo stesso numero di nodi neri .

Useremo DataKinds e GADTs, una potente combinazione di programmazione di livello tipo.

{-# LANGUAGE DataKinds, GADTS, KindSignatures #-} 

import GHC.TypeLits 

In primo luogo, alcuni tipi per rappresentare i colori.

data Colour = Red | Black -- promoted to types via DataKinds 

questo definisce un nuovo tipo Colour abitato da due tipi: Red e Black. Nota che non ci sono valori (ignorando i fondi) che abitano questi tipi, ma non avremo comunque bisogno di loro.

I nodi dell'albero rosso-neri sono rappresentati dai seguenti GADT

-- 'c' is the Colour of the node, either Red or Black 
-- 'n' is the number of black child nodes, a type level Natural number 
-- 'a' is the type of the values this node contains 
data Node (c :: Colour) (n :: Nat) a where 
    -- all leaves are black 
    Leaf :: Node Black 1 a 
    -- black nodes can have children of either colour 
    B :: Node l  n a -> a -> Node r  n a -> Node Black (n + 1) a 
    -- red nodes can only have black children 
    R :: Node Black n a -> a -> Node Black n a -> Node Red n a 

GADT ci permette di esprimere la Colour dei R e B costruttori direttamente nei tipi.

La radice dell'albero assomiglia a questo

data RedBlackTree a where 
    RBTree :: Node Black n a -> RedBlackTree a 

Ora è impossibile creare un ben digitato RedBlackTree che viola uno qualsiasi dei 4 immobili di cui sopra.

1. Il primo vincolo è ovviamente vero, ci sono solo 2 tipi abitano Colour.
2. Dalla definizione di RedBlackTree la radice è nera.
3. Dalla definizione del costruttore Leaf, tutte le foglie sono nere.
4. Dalla definizione del costruttore R, entrambi i figli devono essere i numeri Black . Come pure, il numero di nodi figlio neri di ogni sottostruttura sono uguali (lo stesso n viene utilizzato nel tipo di entrambe le sottostrutture sinistra e destra)

Tutte queste condizioni sono verificate al momento della compilazione da GHC, il che significa che abbiamo non otterrà mai un'eccezione di runtime da un codice anomalo che invalida le nostre ipotesi su un albero rosso-nero. È importante sottolineare che non ci sono costi di runtime associati a questi vantaggi extra, tutto il lavoro viene svolto in fase di compilazione.

Answer 3

Le altre risposte sono molto belle, ma voglio sottolineare un punto. La nostra teoria del linguaggio di programmazione dei termini si basa fortemente sul calcolo Lambda. Un Lisp "puro" corrisponde (più o meno) a un Lambda Calculus non tipizzato pesantemente zuccherato. Il significato dei programmi è definito dalle regole di valutazione che indicano come vengono ridotti i termini del calcolo Lambda durante l'esecuzione del programma.

In una lingua digitata, assegniamo i tipi ai termini. Per ogni regola di valutazione, abbiamo una regola di tipo corrispondente che mostra come i tipi vengono preservati dalla valutazione. A seconda del sistema di tipi, esistono anche altre regole che definiscono il modo in cui i tipi si correlano tra loro. Si scopre che una volta ottenuto un sistema di tipo sufficientemente interessante, i tipi e il loro sistema di regole corrispondono anche a una variante del calcolo Lambda!

Anche se è normale pensare al Lambda Calculus come linguaggio di programmazione ora, è stato originariamente concepito come un sistema di logica. Questo è il motivo per cui è utile ragionare sui tipi di termini in un linguaggio di programmazione. Ma l'aspetto del linguaggio di programmazione di Lambda Calculus consente di scrivere programmi che vengono valutati dal correttore di tipi.

Si spera che ora si possa vedere che la "programmazione a livello di testo" non è una cosa sostanzialmente diversa dalla "programmazione a livello di termine", ma non è molto comune ora avere un linguaggio in un sistema di tipi abbastanza potente che avresti un motivo per scrivere programmi in esso.