title: Parsing an Indexed Type
body: <p>I just started exploring the possibilities of <a href="http://www.cs.ru.nl/~W.Swierstra/Publications/DataTypesALaCarte.pdf" rel="nofollow noreferrer">data types à la carte</a> in combination with indexed types. My current experiment is a bit too large to include here, but can be found <a href="https://gist.github.com/jakubdaniel/6b67eb67b3bd7e2c284a5c68074ed7db" rel="nofollow noreferrer">here</a>. My example is mixing together an expression from different ingredients (arithmetic, functions, ...). The goal is to enforce only well-typed expressions. That is why an index is added to the expressions (the <code>Sort</code> type).</p>
  
  <p>I can build expressions like:</p>
  
  <pre><code>-- define expressions over variables and arithmetic (+, *, numeric constants)
  type Lia = IFix (VarF :+: ArithmeticF)
  
  -- expression of integer type/sort
  t :: Lia IntegralSort
  t = var "c" .+. cnst 1
  </code></pre>
  
  <p>This is all good as long as I construct only fixed (static) expressions.</p>
  
  <p>Is there a way to read an expression from string/other representation (that obviously has to encode the sort) and produce a dynamic value that gets represented by these functors?</p>
  
  <p>For example, I would like to read <code>((c : Int) + (1 : Int))</code> and represent it somehow with <code>VarF</code> and <code>ArithmeticF</code>. Here I realize I cannot obtain a value of static type <code>Lia IntegralSort</code>. But suppose I have in addition:</p>
  
  <pre><code>data EqualityF a where
      Equals :: forall s. a s -&gt; a s -&gt; EqualityF a BoolSort
  </code></pre>
  
  <p>I could expect there being a function that can read <code>String</code> into <code>Maybe (IFix (EqualityF :+: VarF :+: ...))</code>. Such a function would attempt to build representations for the LHS and RHS and if the sorts matched it could produce a result of statically known type <code>IFix (EqualityF :+: ...) BoolSort</code>. The problem is that the representation of LHS (and RHS) has no fixed static sort. Is what I am trying to do impossible with this representation I chose?</p>