F # и статически проверенные случаи объединения - PullRequest
Новая
       4

F # и статически проверенные случаи объединения

7 голосов
/ 11 мая 2010

Вскоре я и мой соратник Джоэл выпустим версию 0.9 Wing Beats . Это внутренний DSL, написанный на F #. С его помощью вы можете генерировать XHTML. Одним из источников вдохновения был модуль XHTML.M платформы Ocsigen. Я не привык к синтаксису OCaml, но я понимаю, что XHTML.M как-то статически проверяет, имеют ли атрибуты и дочерние элементы допустимые типы.

Нам не удалось статически проверить одно и то же в F #, и теперь мне интересно, есть ли у кого-нибудь идеи, как это сделать?

Мой первый наивный подход состоял в том, чтобы представить каждый тип элемента в XHTML как объединенный случай. Но, к сожалению, вы не можете статически ограничить, какие случаи допустимы в качестве значений параметров, как в XHTML.M.

Затем я попытался использовать интерфейсы (каждый тип элемента реализует интерфейс для каждого допустимого родителя) и ограничения типа, но мне не удалось заставить его работать без использования явного приведения таким образом, чтобы сделать решение громоздким для использовать. И все равно это не было элегантным решением.

Сегодня я рассматривал контракты по коду, но, похоже, они несовместимы с F # Interactive. Когда я нажимаю Alt + Enter, он останавливается.

Просто чтобы прояснить мой вопрос. Вот супер простой искусственный пример той же проблемы: 

type Letter = 
    | Vowel of string
    | Consonant of string
let writeVowel = 
    function | Vowel str -> sprintf "%s is a vowel" str

Я хочу, чтобы writeVowel принимал только гласные статически, а не как указано выше, проверяйте его во время выполнения.

Как мы можем достичь этого? У кого-нибудь есть идеи? Там должен быть умный способ сделать это. Если не со случаями объединения, может быть, с интерфейсами? Я боролся с этим, но попал в ловушку и не могу думать вне этого.

Ответы [ 6 ]

4 голосов
/ 12 мая 2010

Похоже, что библиотека использует полиморфные варианты О'Камла, которые недоступны в F #. К сожалению, я также не знаю верного способа кодировать их в F #.

Одной из возможностей может быть использование «фантомных типов», хотя я подозреваю, что это может стать громоздким, учитывая количество различных категорий контента, с которыми вы имеете дело. Вот как вы могли бы справиться со своим примером гласного: 

module Letters = begin
  (* type level versions of true and false *)
  type ok = class end
  type nok = class end

  type letter<'isVowel,'isConsonant> = private Letter of char

  let vowel v : letter<ok,nok> = Letter v
  let consonant c : letter<nok,ok> = Letter c
  let y : letter<ok,ok> = Letter 'y'

  let writeVowel (Letter(l):letter<ok,_>) = sprintf "%c is a vowel" l
  let writeConsonant (Letter(l):letter<_,ok>) = sprintf "%c is a consonant" l
end

open Letters
let a = vowel 'a'
let b = consonant 'b'
let y = y

writeVowel a
//writeVowel b
writeVowel y
2 голосов
/ 14 мая 2010

Вы можете использовать встроенные функции со статически разрешенными параметрами типов для получения различных типов в зависимости от контекста. 

let inline pcdata (pcdata : string) : ^U = (^U : (static member MakePCData : string -> ^U) pcdata)
let inline a (content : ^T) : ^U = (^U : (static member MakeA : ^T -> ^U) content)        
let inline br () : ^U = (^U : (static member MakeBr : unit -> ^U) ())
let inline img () : ^U = (^U : (static member MakeImg : unit -> ^U) ())
let inline span (content : ^T) : ^U = (^U : (static member MakeSpan : ^T -> ^U) content)

Возьмите, например, функцию br. Он выдаст значение типа ^ U, которое статически разрешается при компиляции. Это скомпилируется, только если ^ U имеет статический член MakeBr. Учитывая приведенный ниже пример, это может привести к созданию A_Content.Br или Span_Content.Br.

Затем вы определяете набор типов для представления легального контента. Каждый выставляет «Make» участников для контента, который он принимает. 

type A_Content =
| PCData of string
| Br
| Span of Span_Content list
        static member inline MakePCData (pcdata : string) = PCData pcdata
        static member inline MakeA (pcdata : string) = PCData pcdata
        static member inline MakeBr () = Br
        static member inline MakeSpan (pcdata : string) = Span [Span_Content.PCData pcdata]
        static member inline MakeSpan content = Span content

and Span_Content =
| PCData of string
| A of A_Content list
| Br
| Img
| Span of Span_Content list
    with
        static member inline MakePCData (pcdata : string) = PCData pcdata
        static member inline MakeA (pcdata : string) = A_Content.PCData pcdata
        static member inline MakeA content = A content
        static member inline MakeBr () = Br
        static member inline MakeImg () = Img
        static member inline MakeSpan (pcdata : string) = Span [PCData pcdata]
        static member inline MakeSpan content = Span content

and Span =
| Span of Span_Content list
        static member inline MakeSpan (pcdata : string) = Span [Span_Content.PCData pcdata]
        static member inline MakeSpan content = Span content

Затем вы можете создавать значения ... 

let _ =
    test ( span "hello" )
    test ( span [pcdata "hello"] )
    test (
        span [
            br ();
            span [
                br ();
                a [span "Click me"];
                pcdata "huh?";
                img () ] ] )

Используемая там тестовая функция печатает XML ... Этот код показывает, что значения приемлемы для работы. 

let rec stringOfAContent (aContent : A_Content) =
    match aContent with
    | A_Content.PCData pcdata -> pcdata
    | A_Content.Br -> "<br />"
    | A_Content.Span spanContent -> stringOfSpan (Span.Span spanContent)

and stringOfSpanContent (spanContent : Span_Content) =
    match spanContent with
    | Span_Content.PCData pcdata -> pcdata
    | Span_Content.A aContent ->
        let content = String.concat "" (List.map stringOfAContent aContent)
        sprintf "<a>%s</a>" content
    | Span_Content.Br -> "<br />"
    | Span_Content.Img -> "<img />"
    | Span_Content.Span spanContent -> stringOfSpan (Span.Span spanContent)

and stringOfSpan (span : Span) =
    match span with
    | Span.Span spanContent ->
        let content = String.concat "" (List.map stringOfSpanContent spanContent)
        sprintf "<span>%s</span>" content

let test span = printfn "span: %s\n" (stringOfSpan span)

Вот вывод: 

span: <span>hello</span>

span: <span><br /><span><br /><a><span>Click me</span></a>huh?<img /></span></span>

Сообщения об ошибках кажутся разумными ... 

test ( div "hello" )

Error: The type 'Span' does not support any operators named 'MakeDiv'

Поскольку функции Make и другие функции являются встроенными, сгенерированный IL, вероятно, аналогичен тому, что вы могли бы кодировать вручную, если бы вы реализовывали это без добавления безопасного типа.

Вы можете использовать тот же подход для обработки атрибутов.

Мне интересно, ухудшится ли он по швам, как Брайан указал на решения, позволяющие искажать. (Считается ли это контрационистом или нет?) Или, если к тому моменту, когда он реализует весь XHTML, он растопит компилятор или разработчика.

2 голосов
/ 12 мая 2010

Мое скромное предложение: если система типов не может легко поддерживать статическую проверку «X», не проходите нелепые искажения, пытаясь статически проверить «X». Просто выбросить исключение во время выполнения. Небо не упадет, мир не кончится.

Смешные искажения для получения статической проверки часто происходят за счет усложнения API, делают сообщения об ошибках непонятными и вызывают другие искажения в швах.

2 голосов
/ 11 мая 2010

Строго говоря, если вы хотите различать что-то во время компиляции, вам нужно дать ему разные типы. В вашем примере вы можете определить два типа букв, и тогда тип Letter будет либо первым, либо вторым.

Это немного громоздко, но, вероятно, это единственный прямой способ достичь того, чего вы хотите: 

type Vowel = Vowel of string
type Consonant = Consonant of string
type Letter = Choice<Vowel, Consonant>

let writeVowel (Vowel str) = sprintf "%s is a vowel" str
writeVowel (Vowel "a") // ok
writeVowel (Consonant "a") // doesn't compile

let writeLetter = function
  | Choice1Of2(Vowel str) -> sprintf "%s is a vowel" str
  | Choice2Of2(Consonant str) -> sprintf "%s is a consonant" str

Тип Choice - это простое распознаваемое объединение, которое может хранить либо значение первого типа, либо значение второго типа - вы можете определить свой собственный распознаваемый союз, но придумать разумный подход довольно сложно. имена для случаев объединения (из-за вложенности).

Кодовые контракты позволяют вам задавать свойства на основе значений, которые были бы более подходящими в этом случае. Я думаю, что они должны работать с F # (при создании приложения F #), но у меня нет опыта их интеграции с F #.

Для числовых типов вы также можете использовать единицы измерения , которые позволяют добавлять дополнительную информацию к типу (например, число имеет тип float<kilometer>), но это недоступно для string. Если бы это было так, вы могли бы определить единицы измерения vowel и consonant и написать string<vowel> и string<consonant>, но единицы измерения фокусируются в основном на численных приложениях.

Так что, возможно, лучший вариант - в некоторых случаях полагаться на проверки во время выполнения.

[EDIT] Чтобы добавить некоторые детали относительно реализации OCaml - я думаю, что хитрость, которая делает это возможным в OCaml, заключается в том, что он использует структурный подтип, что означает (в переводе на термины F #) может определить дискриминированный союз с некоторыми членами (например, только Vowel), а затем другой с большим количеством членов (Vowel и Consonant).

Когда вы создаете значение Vowel "a", его можно использовать в качестве аргумента для функций, принимающих любой из типов, но значение Consonant "a" можно использовать только с функциями, принимающими второй тип.

Это, к сожалению, не может быть легко добавлено в F #, потому что .NET изначально не поддерживает структурные подтипы (хотя это может быть возможно с использованием некоторых приемов в .NET 4.0, но это должно быть сделано компилятором). Итак, я знаю, понимаю вашу проблему, но не знаю, как ее решить.

Некоторая форма структурного подтипирования может быть выполнена с использованием статических ограничений членов в F #, но, поскольку случаи дискриминационного объединения не являются типами с точки зрения F #, я не думаю, что это пригодно для использования здесь.

1 голос
/ 13 мая 2010

Спасибо за все предложения! На всякий случай это вдохновит любого найти решение проблемы: ниже приведена простая HTML-страница, написанная на нашем DSL Wing Beats. Пролет - это дитя тела. Это не правильный HTML. Было бы хорошо, если бы он не компилировался. 

let page =
    e.Html [
        e.Head [ e.Title & "A little page" ]
        e.Body [
            e.Span & "I'm not allowed here! Because I'm not a block element."
        ]
    ]

Или есть другие способы проверить это, о которых мы не подумали? Мы прагматичны! Любой возможный способ стоит исследовать. Одна из основных целей Wing Beats - заставить его работать как экспертная система (X) Html, которой руководствуется программист. Мы хотим быть уверены, что программист создает недействительный (X) HTML только по своему усмотрению, а не из-за недостатка знаний или небрежных ошибок.

Мы думаем, что у нас есть решение для статической проверки атрибутов. Это выглядит так: 

module a = 
    type ImgAttributes = { Src : string; Alt : string; (* and so forth *) }
    let Img = { Src = ""; Alt = ""; (* and so forth *) }
let link = e.Img { a.Img with Src = "image.jpg"; Alt = "An example image" };

У него есть свои плюсы и минусы, но он должен работать.

Ну, если кто-нибудь что-нибудь придумает, дайте нам знать!

1 голос
/ 12 мая 2010

Классы 

type Letter (c) =
    member this.Character = c
    override this.ToString () = sprintf "letter '%c'" c

type Vowel (c) = inherit Letter (c)

type Consonant (c) = inherit Letter (c)

let printLetter (letter : Letter) =
    printfn "The letter is %c" letter.Character

let printVowel (vowel : Vowel) =
    printfn "The vowel is %c" vowel.Character

let _ =
    let a = Vowel('a')
    let b = Consonant('b')
    let x = Letter('x')

    printLetter a
    printLetter b
    printLetter x

    printVowel a
//    printVowel b  // Won't compile

    let l : Letter list = [a; b; x]
    printfn "The list is %A" l
...