-1
$\begingroup$

Wondering if/how you could define a highly nested structure as a Dependent Type (or an Algebraic or Parameterized type). Specifically, an HTML template. Not that they work like this (HTML templates don't have variables to plug in), but imagine a template like this:

<template id="MyTemplate">
  <section>
    <header>
      <h1>{title}</h1>
      <h2>{subtitle}</h2>
    </header>
    <div>{content}</div>
    <footer>
      <cite>{author}</cite>
      <time>{year}</time>
    </footer>
  </section>
</template>

This is a template, so it basically acts like a class (or a type). So you would instantiate the type like this:

var node = new MyTemplate({
  title: 'A title',
  subtitle: 'A subtitle',
  content: 'Foo bar ...',
  author: 'foo@example',
  year: 2018
})

And you would get:

<section>
  <header>
    <h1>A title</h1>
    <h2>A subtitle</h2>
  </header>
  <div>Foo bar ...</div>
  <footer>
    <cite>foo@example</cite>
    <time>2018</time>
  </footer>
</section>

The HTML node that is returned is like the type instance. (I'm assuming these are HTMLEntity objects and related DOM objects, not strings). The way the DOM node instances are generically represented is:

{
  tag: 'section',
  children: [
    {
      tag: 'header',
      children: [ ... ]
    },
    ...
  ]
}

But the template, being a type, is like it is defining multiple nested types at once. That is, this is a type:

<h1>{title}</h1>

And that is wrapped in this type:

<header>
  <h1>{title}</h1>
  <h2>{subtitle}</h2>
</header>

And that is wrapped in the <section>...</section> type. It's like a type like this:

type Section {
  type Header {
    type H1 {
      title: String
    }
    type H2 {
      subtitle: String
    }
  },
  type Div {
    content: String
  },
  type Footer {
    type H1 {
      cite: String
    }
    type H2 {
      time: Integer
    }
  }
}

Or perhaps, since we are actually plugging this into the HTMLEntity's textContent property, it would be more like this:

type Section {
  type Header {
    type H1 {
      title: String
      where textContent = title
    }
    type H2 {
      subtitle: String
      where textContent = title
    }
  },
  ...
}

Either way, wondering if you can do anything like that in Haskell, or another type-theory-oriented language like Coq.

In Haskell, a (binary) tree is represented as a recursive structure:

data Tree a = Nil | Node a (Tree a) (Tree a)

I don't know much Haskell, so I'm not sure how to represent the above HTML template "type" as a Haskell algebraic type (or if it is possible). But it seems like it could be defined as some form of an algebraic or a parameterized type.

My first question is, the kind of type the template can be called, and how to model it as a type (in Haskell, or Coq, or some language using a lot of type theory).

The second question is if an extended version of this template, which has looping, would be considered a dependent type (and then how to model it as a dependent type). That might look like this.

<template id="MyTemplateWithIteration">
  <section>
    <header>
      <h1>{title}</h1>
      <h2>{subtitle}</h2>
    </header>
    <ul>
    {each label in labels}
      <li>{label}</li>
    {/each}
    </ul>
    <footer>
      <cite>{author}</cite>
      <time>{year}</time>
    </footer>
  </section>
</template>

The reason I am thinking this could potentially be a dependent type is because dependent types deal with "forall", which seems like what the iteration is doing. Might be misunderstanding that part.

To finish up, what I normally just do is create a template object, instead of a type, and then from the template object you create an instance of some other type (the HTMLEntity in this case). But it seems like this could be formalized some more, and instead of a template object we could upgrade it to a template type, and then we would just be creating a template instance when instantiating it. Hoping to see how that definition would look for this highly nested structure.

Related note, wondering if this (modeling natural language trees using types) is similar. I'm not sure if they are modeling tree as a type, or just the nodes as types. Or perhaps grammars are nested types of some sort.

$\endgroup$
  • 2
    $\begingroup$ Is this going to turn into “define every imaginable object as a dependent type”? These long code blocks make these questions look very much like off-topic programming questions. What, really, is the difference between “write a program that does X” and “write a type that does X”? $\endgroup$ – David Richerby Jul 8 '18 at 16:42
3
$\begingroup$

You might be looking for CDuce programming language.

$\endgroup$
2
$\begingroup$

You might also be interested in the Ur/Web programming language.

$\endgroup$

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.