2
$\begingroup$

Would be possible to encode dependent types as regular expressions? if so, ¿is there some work about?

It's common to represent restrictions for elements in a traversable data structure with them, like clojure.spec do for sequences. But i tried to find some references about using them to represent restrictions at type level with no luck.

Some examples in seudo haskell syntax:

unboundInts :: Int *
-- accepted by typechecker
unboundInts = [] | [1] | [1..] | ["whatever",1,1.2]
-- rejected
unboundInts = ["whatever"]

threeIntsAndChars :: ^ Int {3} Char + $
-- accepted
threeIntsAndChars = [1,2,3,'a'] | [4,5,6,'a'..'z']
-- rejected
threeIntsAndChars = [] | ["whatever",1,2,3,'a'] | [1,2,3,'a',"whatever"] | [1,2,3] | [1,2,'a'] | ...

-- accepted
data Tree a = Empty | Leaf a | Node (Tree a) a (Tree a)
threeIntsAndChars = Node (Node (Leaf 1) 2 (leaf 3)) 'a' (Leaf 'b')  
$\endgroup$
  • 1
    $\begingroup$ Welcome to CS.SE! What properties do you want the encoding to have? It's probably possible to do something, but it's not clear exactly what properties you want the encoding to have and what you want to be able to do with the encoding. Also note that you might prefer a regular tree grammar over a regexp, for tree-shaped data structures. $\endgroup$ – D.W. Dec 5 '16 at 18:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.