Typechecking Error

Google Group
1

Hi there,

I have a part of my code that doesn’t type-check and that I cannot
understand
why it doesn’t type-check. I would appreciate it if you could help me find
the
problem:

Here are the datatype definitions:

datatype Answer(int, int) =
| True(0, 0) of ()
| False(0, 1) of ()
| Unknown(0, 2) of ()
| {x:nat} {k:nat} Decision(x+1, k) of
[x_l:nat | x_l <= x] [k_l:nat]
[x_r:nat | x_r <= x+1] [k_r:nat | (k_r > k && x_r == x+1) || (x_r <= x
)]
(int(x), int(k), Answer(x_l, k_l), Answer(x_r, k_r))
// if x_n <= v then Answer(n_l, v_l) else Answer(n_r, v_r)

typedef Answer0 = [n:int] [v:int] Answer(n, v)
typedef NodeKey = (int, int, Answer0, Answer0) // Variable + Value +
LEqAnswer + GTAnswer

And here is the code that that doesn’t type-check:

fun GetNode
{x:nat} {k:nat} {x_l:nat | x_l <= x} {k_l:nat}
{x_r:nat | x_r <= x + 1} {k_r:nat | (x_r <= x) || ((x_r == x + 1) &&k_r

k)}
(x:int(x), k:int(k),
lte_answer:Answer(x_l, k_l), gt_answer:Answer(x_r, k_r),
nodes: &map(NodeKey, Answer0)) : Answer0 =
let
val key = (x, k, lte_answer, gt_answer)
val cachedNode = funmap_search_opt(nodes, key)
in
case+ cachedNode of
| ~Some_vt(node) => node
| ~None_vt() =>
let
val new_node = Decision(x, k, lte_answer, gt_answer)
in
nodes.insert(key, new_node) ; new_node
end
end

The position of error is on the line “val new_node = Decision(…)” where
it essentially says that Decision(…) cannot be type-checked. However,
given the conditions on x, k, x_l, k_l, x_r and k_r guaranteed by function
GetNode, I cannot see why there is an error.

Please let me know what I have missed :slight_smile:

Thanks,
Shahab

2

After seeing your code, I have to say that I am a bit concerned with the
complexity involved in the definition of Answer.

Usually, one starts with non-dependent datatypes and later replace them
with dependent versions (if really needed). Starting with a datatype like
Answer
could complicate programming very quickly from very early on.On Wednesday, March 26, 2014 2:58:40 PM UTC-4, Shahab Tasharrofi wrote:

Hi there,

I have a part of my code that doesn’t type-check and that I cannot
understand
why it doesn’t type-check. I would appreciate it if you could help me find
the
problem:

Here are the datatype definitions:

datatype Answer(int, int) =
| True(0, 0) of ()
| False(0, 1) of ()
| Unknown(0, 2) of ()
| {x:nat} {k:nat} Decision(x+1, k) of
[x_l:nat | x_l <= x] [k_l:nat]
[x_r:nat | x_r <= x+1] [k_r:nat | (k_r > k && x_r == x+1) || (x_r <=x
)]
(int(x), int(k), Answer(x_l, k_l), Answer(x_r, k_r))
// if x_n <= v then Answer(n_l, v_l) else Answer(n_r, v_r)

typedef Answer0 = [n:int] [v:int] Answer(n, v)
typedef NodeKey = (int, int, Answer0, Answer0) // Variable + Value +
LEqAnswer + GTAnswer

And here is the code that that doesn’t type-check:

fun GetNode
{x:nat} {k:nat} {x_l:nat | x_l <= x} {k_l:nat}
{x_r:nat | x_r <= x + 1} {k_r:nat | (x_r <= x) || ((x_r == x + 1) &&k_r

k)}
(x:int(x), k:int(k),
lte_answer:Answer(x_l, k_l), gt_answer:Answer(x_r, k_r),
nodes: &map(NodeKey, Answer0)) : Answer0 =
let
val key = (x, k, lte_answer, gt_answer)
val cachedNode = funmap_search_opt(nodes, key)
in
case+ cachedNode of
| ~Some_vt(node) => node
| ~None_vt() =>
let
val new_node = Decision(x, k, lte_answer, gt_answer)
in
nodes.insert(key, new_node) ; new_node
end
end

The position of error is on the line “val new_node = Decision(…)” where
it essentially says that Decision(…) cannot be type-checked. However,
given the conditions on x, k, x_l, k_l, x_r and k_r guaranteed by function
GetNode, I cannot see why there is an error.

Please let me know what I have missed :slight_smile:

Thanks,
Shahab

3

Okay, I found what the problem was. In the datatype definition, I should
have
universally quantified x_l, x_r, k_l and k_r.

Shahab